アサーション自動生成とそのシミュレーションによる完全検証

• Item type: SIG Technical Reports(1)
• 公開日: 2014-03-08
• タイトル: アサーション自動生成とそのシミュレーションによる完全検証
• タイトル / 言語: en
• タイトル: Automatic Generation of Assertions and their Formal Verification through Simulations
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 検証技術
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 東京大学大規模集積システム設計教育研究センター
• 著者所属: 東京大学大規模集積システム設計教育研究センター
• 著者所属: 東京大学大学院工学系研究科電気系工学専攻
• 著者所属(英): en
• 著者所属(英): VLSI Design and Education Center, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): VLSI Design and Education Center, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Dept. of Electrical Engineering and Information Systems, The University of Tokyo
• 著者名: 藤田, 昌宏; 松本, 剛史; 城, 怜史
• 著者名(英): Masahiro, Fujita; Takeshi, Matsumoto; Satoshi, Jo
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: アサーションベース検証は、SoC に代表される大規模ハードウェア設計に対するもっとも効果的な検証手法の 1 つとして広く利用されている。検証品質は、チェックしたアサーションの質と量に依存するが、人手で十分なアサーションを迅速に用意することは現実には難しい。このため、仕様や設計記述からアサーションを自動生成する技術が研究開発されている。正しくない設計記述から生成されたアサーションは誤っている可能性があるが、自動生成されたアサーションを設計者が検査することにより、有益な情報として処理できる。本稿では、与えられた外部あるいは内部信号間の論理的な関係を一般的に抽出する新規手法の提案と、それを組合せ回路 （あるいは時間軸方向に一定数展開された順序回路） に適用した実験結果について報告する。 LUT （Look Up Table） で表現することで、数万ゲート規模の回路中の与えられた信号間に存在する論理的な関係を SAT ソルバーにより効率的に求めることができる。手法自体は、組み込みシステム一般にも適用できる。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Assertion Based Verification (ABV) is one of the most important verification methods for SoC and complicated hardware system designs. Quality of verification depends on the amount of assertions checked, but it may not be easy to prepare sufficient assertions by designers. There have been works which try to automatically generate assertions from specification and/or design description. Although possibly incorrect assertions may be generated from buggy designs, by the analysis on generated assertions with designers, even such information could be useful. In this paper, we propose a new method by which logical relationships among internal and external signals can be extracted and present its experimental results applied to combinational circuits. With a formulation of the problem using LUT (Look Up Table), assertions on circuits having tens of thousands gates can efficiently be generated using SAT solvers. The proposed method can be applied to embedded systems in general.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA12149313
• 書誌情報: 研究報告組込みシステム（EMB）; 巻 2014-EMB-32, 号 17, p. 1-6, 発行日 2014-03-08
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会