{"links":{},"id":27041,"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00027041","sets":["1164:2036:2049:2052"]},"path":["2052"],"owner":"1","recid":"27041","title":["動作合成前後の設計記述に対する記号シミュレーションによる形式的等価性検証の検討"],"pubdate":{"attribute_name":"公開日","attribute_value":"2006-05-12"},"_buckets":{"deposit":"a9f8ab4d-b616-4171-bdf0-b7d3a27a6d5f"},"_deposit":{"id":"27041","pid":{"type":"depid","value":"27041","revision_id":0},"owners":[1],"status":"published","created_by":1},"item_title":"動作合成前後の設計記述に対する記号シミュレーションによる形式的等価性検証の検討","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"動作合成前後の設計記述に対する記号シミュレーションによる形式的等価性検証の検討"},{"subitem_title":"An Approach to Equivalence Checking by Symbolic Simulation between Behavioral and RTL Designs","subitem_title_language":"en"}]},"item_type_id":"4","publish_date":"2006-05-12","item_4_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"東京大学大学院工学系研究科電子工学専攻"},{"subitem_text_value":"東京大学大規模集積システム設計教育研究センター"},{"subitem_text_value":"東京大学大規模集積システム設計教育研究センター"}]},"item_4_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Dept. of Electronics Engineering, University of Tokyo","subitem_text_language":"en"},{"subitem_text_value":"VLSI Design and Education Center, University of Tokyo","subitem_text_language":"en"},{"subitem_text_value":"VLSI Design and Education Center, University of Tokyo","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/27041/files/IPSJ-SLDM06125007.pdf"},"date":[{"dateType":"Available","dateValue":"2008-05-12"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-SLDM06125007.pdf","filesize":[{"value":"633.7 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"10"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"d848c6c9-43d7-48e0-bf56-17b16087ae07","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2006 by the Information Processing Society of Japan"}]},"item_4_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"松本, 剛史"},{"creatorName":"小松, 聡"},{"creatorName":"藤田, 昌宏"}],"nameIdentifiers":[{}]}]},"item_4_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Takeshi, MATSUMOTO","creatorNameLang":"en"},{"creatorName":"Satoshi, KOMATSU","creatorNameLang":"en"},{"creatorName":"Masahiro, FUJITA","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_4_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA11451459","subitem_source_identifier_type":"NCID"}]},"item_4_textarea_12":{"attribute_name":"Notice","attribute_value_mlt":[{"subitem_textarea_value":"SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc."}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_18gh","resourcetype":"technical report"}]},"item_4_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"システムレベル設計によって得られた動作記述と制約から、動作合成によってＲＴＬ設計を導出する設計フローにおいては、動作合成前後の動作記述とＲＴＬ設計の動作の等価性が保証されていることが重要である。しかし、そのための等価性検証手法、特に形式的手法は、実用化されているものはほとんどないのが現状である。そこで、本稿では、動作合成前後の設計の等価性を形式的に検証する一手法を提案し、その評価を行う。提案する手法では、ＲＴＬ設計を解析して抽出された、１サイクルで行われる動作と、合成前の動作記述を記号的に実行して、形式的に等価性を検証する。ＲＴＬ設計から動作を抽出する作業では、いくつかの変換規則を適用することによって、ＲＴＬ設計中のビット結合などのビットレベル処理をワードレベルの処理に置き換え、個々の演算を解釈せずに検証が可能になるようにしている。また、いくつかの設計例に対して実験を行い、指定された適当な等価性を検証できることを確認した。","subitem_description_type":"Other"}]},"item_4_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"ln system-level design，RTL designs are generated by behavioral synthesizers from behavior descriptions, and the equivalence between designs before and after behaviral synthesis should be guaranteed. However, few verification methods，especially formal ones，are available for this purpose. ln this paper, we propose a method to formally verify the equivalence. In the method, behaviors executed in a clock cycle in RTL designs are extracted，and symbolically simulated with the original behavior descriptions. When extracting behaviors from RTL designs，several rules are applied to translate bit-level operations in RTL into word-level ones so that the equivalence can be verified uninterpretedly. Also, we show the experimental results on some design examples.","subitem_description_type":"Other"}]},"item_4_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"42","bibliographic_titles":[{"bibliographic_title":"情報処理学会研究報告システムLSI設計技術（SLDM）"}],"bibliographicPageStart":"37","bibliographicIssueDates":{"bibliographicIssueDate":"2006-05-12","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"41(2006-SLDM-125)","bibliographicVolumeNumber":"2006"}]},"relation_version_is_last":true,"weko_creator_id":"1"},"created":"2025-01-18T22:57:30.228218+00:00","updated":"2025-01-22T18:43:36.076448+00:00"}