動作合成前後の設計記述に対する記号シミュレーションによる形式的等価性検証の検討

• Item type: SIG Technical Reports(1)
• 公開日: 2006-05-12
• タイトル: 動作合成前後の設計記述に対する記号シミュレーションによる形式的等価性検証の検討
• タイトル / 言語: en
• タイトル: An Approach to Equivalence Checking by Symbolic Simulation between Behavioral and RTL Designs
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 東京大学大学院工学系研究科電子工学専攻
• 著者所属: 東京大学大規模集積システム設計教育研究センター
• 著者所属: 東京大学大規模集積システム設計教育研究センター
• 著者所属(英): en
• 著者所属(英): Dept. of Electronics Engineering, University of Tokyo
• 著者所属(英): en
• 著者所属(英): VLSI Design and Education Center, University of Tokyo
• 著者所属(英): en
• 著者所属(英): VLSI Design and Education Center, University of Tokyo
• 著者名: 松本, 剛史; 小松, 聡; 藤田, 昌宏
• 著者名(英): Takeshi, MATSUMOTO; Satoshi, KOMATSU; Masahiro, FUJITA
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: システムレベル設計によって得られた動作記述と制約から、動作合成によってＲＴＬ設計を導出する設計フローにおいては、動作合成前後の動作記述とＲＴＬ設計の動作の等価性が保証されていることが重要である。しかし、そのための等価性検証手法、特に形式的手法は、実用化されているものはほとんどないのが現状である。そこで、本稿では、動作合成前後の設計の等価性を形式的に検証する一手法を提案し、その評価を行う。提案する手法では、ＲＴＬ設計を解析して抽出された、１サイクルで行われる動作と、合成前の動作記述を記号的に実行して、形式的に等価性を検証する。ＲＴＬ設計から動作を抽出する作業では、いくつかの変換規則を適用することによって、ＲＴＬ設計中のビット結合などのビットレベル処理をワードレベルの処理に置き換え、個々の演算を解釈せずに検証が可能になるようにしている。また、いくつかの設計例に対して実験を行い、指定された適当な等価性を検証できることを確認した。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11451459
• 書誌情報: 情報処理学会研究報告システムLSI設計技術（SLDM）; 巻 2006, 号 41(2006-SLDM-125), p. 37-42, 発行日 2006-05-12
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会