2012 Fiscal Year Annual Research Report
フォーマル手法およびシミュレーション手法の統合によるハードウェア検証の効率化
| Project/Area Number |
22500047
|
|---|
| Research Institution | Shimane University |
|---|
Principal Investigator |
浜口 清治 島根大学, 総合理工学研究科(研究院), 教授 (80238055)
|
|---|
| Project Period (FY) |
2010-04-01 – 2013-03-31
|
| Keywords | 設計検証技術 / フォーマル検証 / シミュレーションベース検証 / SATソルバ / 有界モデル検査 / カバレッジ駆動検証 |
|---|
| Research Abstract |
SoC(システム・オン・チップ)など大規模な集積回路の設計においては，設計検証工程の効率化が依然課題となっている．主な技術として，シミュレーション手法とフォーマル検証手法が用いられているが，この２つの方式はばらばらに適用されているのが実情である．２つの方式を統合する方法については，ほとんど研究が行われていない．本研究では，一方の方式で検証を行った場合の結果を，他方の方式での検証に利用する手法の確立を目指している．
24年度は，23年度に検討・実験した，有界モデル検査においてSATソルバから得られる途中結果を，シミュレーション用テストベンチで制約として与える手法を，より実用的な設計例に対して適用する実験を行った．この手法は，複雑な論理条件を含む設計例では，カバレッジの改善に有効であることが，前年度の予備実験で確認されていたが，実用例では実際に効果がある例を確認することができなかった．このため，SATソルバの利用方法を改変することとした．具体的にはランダムシミュレーションではカバレッジをあげにくい信号線に対して，できるだけ異なるパターンを複数生成するように改変したSAT ソルバを適用することとした．このようにして得られたシミュレーションパタンをテストベンチで用いることによって，値を変えにくい信号線の値をより多く変化させることにより，全体のカバレッジを増大させる．特にトグルカバレッジに注目して，この手法を設計例に適用したところ，内部の状態変化のための論理条件が複雑であるような設計例に対しては，ランダムシミュレーションではカバーできなかったポイントをカバーできるようになり，また，カバーしにくかった信号線を特定の評価指標で評価したところ，２倍以上のトグル発生の改善が確認できた．
|
| Current Status of Research Progress |
Reason
24年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
24年度が最終年度であるため、記入しない。
|
Research Products
(1 results)
