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