2010 Fiscal Year Annual Research Report
フォーマル手法およびシミュレーション手法の統合によるハードウェア検証の効率化
| Project/Area Number |
22500047
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
浜口 清治 大阪大学, 大学院・情報科学研究科, 准教授 (80238055)
|
|---|
| Keywords | フォーマル検証 / シミュレーションベース検証 / SATソルバ / 有界モデル検査 / 制約付きランダムパタン生成 / カバレッジ駆動検証 / アサーションベース検証 |
|---|
| Research Abstract |
SoC(システム・オン・チップ)など大規模な集積回路の設計においては,設計検証工程の効率化が依然課題となっている.これに対処すべく,近年,多くの新しい手法や技術が提唱・実用化が進んでいる.主な技術として,シミュレーション手法とフォーマル検証手法が用いられているが,この2つの方式はばらばらに適用されているのが実情である.2つの方式を統合する方法については,ほとんど研究が行われていない.本研究では,一方の方式で検証を行った場合の結果を,他方の方式での検証に利用する手法の確立を目指す.さらに,2つの方式をタイトに組み合わせることにより,より網羅性の高いシームレスな検証結果を効率よく得る手法の確立を目指す
本年度は,まず,フォーマル検証の過程で得られる中間的な情報を,シミュレーション手法に転用する手法について検討した.有界モデル検査手法をベースとした手法の検討を行った.有界モデル検査では,SATソルバーが内部エンジンとして用いられているが,有界モデル検査を行ったときに,生成される矛盾節と呼ばれる論理式を,SATソルバー実行時に取り出して,その後,シミュレーション用テストベンチにおいて,制約(満足しなければならない条件)として与えるアルゴリズムを確定した.シミュレーションにおける制約は,制約付きランダムパタン生成の利用を想定しているが,シミュレーションは有界モデル検査と異なり,制約が各サイクル毎に独立して有効になるため,複数のサイクルにまたがる制約を処理することができない.このため,1サイクルにのみ言及している制約を用いることを考えている.現在,考案したアルゴリズムについて実装を進めている
|
Research Products
(1 results)
