フォーマル手法およびシミュレーション手法の統合によるハードウェア検証の効率化

2011 Fiscal Year Annual Research Report

• Project/Area Number: 22500047
• Research Institution: Osaka University
• Principal Investigator: 浜口 清治 大阪大学, 大学院・情報科学研究科, 准教授 (80238055)
• Keywords: フォーマル検証 / シミュレーションベース検証 / SATソルバ / 有界モデル検査 / 制約付きランダムパタン生成 / カバレッジ駆動検証 / アサーションベース検証

Research Abstract

SoC(システム・オン・チップ)など大規模な集積回路の設計においては,設計検証工程の効率化が依然課題となっている.主な技術として,シミュレーション手法とフォーマル検証手法が用いられているが,この2つの方式はばらばらに適用されているのが実情である.2つの方式を統合する方法については,ほとんど研究が行われていない.本研究では,一方の方式で検証を行った場合の結果を,他方の方式での検証に利用する手法の確立を目指す.さらに,2つの方式を組み合わせることにより,より網羅性の高い検証結果を得る手法の確立を目指す.
23年度は,22年度に検討した,有界モデル検査の途中で得られる矛盾節をシミュレーション用テストベンチで制約として与える手法の実装を主として行った.シミュレーションでは制約が各サイクル毎に独立して有効になるため,複数のサイクルにまたがる制約を処理することができず,1サイクルのみに言及している制約を用いている.人工的に作成した小規模な順序機械の例に対しては,ランダムシミュレーションでは,3時間以上かかってもカバーできない状態に,本手法では20秒前後で到達できることを確認できた.現在,この結果をもとに,さらに実用的な例題について実験を進めようとしている.そのためには,ハードウェア記述言語によって作成された設計例からSATソルバーに入力するための記述を得て,本手法により得られた制約を元の設計記述に埋め込む必要がある.商用ツールを利用してこの変換を行うと最適化機能により,制約と元の記述との対応関係が大きく損なわれ,本手法の効果が確認できないことが判明した.フォーマル検証実験用に作成されたベンチマーク例題を用いた計算機実験を行うよう変更して,このために変換ツールの実装を行っている.並行して,シミュレーション結果をフォーマル検証に利用する手法についても検討を行った.

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

小規模な例題では効果を確認できたが,実設計例に対しては,9.で述べたように,利用している商用ツールの特性によって,効果を確認するための計算機実験を行うことができなかったため.

Strategy for Future Research Activity

基本的には本来の計画通り実装と計算機実験を進める予定である.ただし,上記で述べたようにツール上の問題については,フォーマル検証実験用のベンチマークを利用することにより対応する予定であり,変換ツールの作成などそのための準備を進めている.