2006 Fiscal Year Annual Research Report
類似度を考慮した等価論理を用いたハードウェアの高位設計検証手法の研究
| Project/Area Number |
17500047
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
木村 晋二 早稲田大学, 大学院情報生産システム研究科, 教授 (20183303)
|
|---|
| Keywords | 等価論理 / ハードウェアの等価検証 / 無評価関数 / 項書き換え |
|---|
| Research Abstract |
類似度を考慮した等価論理を用いたハードウェアの高位設計検証手法について、本年度は、以下のテーマについて研究を行った。
まず、Verilogのハードウェア記述を等価論理の論理式に変換するツールのプロトタイプを完成させた。同時に、複数クロック後の動作を解析するために等価論理の式を時間展開するツールを作成した。このツールは、1クロック分の動作を表す等価論理式を入力とし、それを指定した時間分コピーするとともに、参照される変数と代入される変数に異なる時間を割り当てる。同じ機能を異なるアルゴリズムで実現するVerilog記述を作成し、これらの等価性を判定した。等価論理の判定アルゴリズムが時間展開の数に対して指数的な計算時間を必要とすることと、中間的な等価性の導入により計算時間を削減できることがわかった。また、C言語を等価論理式に変換するツールについても実現と改良を行った。
第二に、等価論理式の等価性判定アルゴリズムに関する文献調査と、CNF式のSATアルゴリズムを適用する手法について検討を行った。とくに、ShostakおよびNelson-Oppenの手法について調査した。
第三に、類似度の双対概念である誤差の解析について、非線形プログラミングの問題に帰着して解く手法の研究を行った。類似度を用いて、ループの展開において、異なる展開を行った結果の中間変数が近いかどうかなどの情報を用いて、中間の等価点を探す手法の検討を行った。
第四に、プロパティ検証のカバレージ手法の、等価検証への応用に関する検討を行った。プロパティ検証のカバレージでは、記述されたプロパティが回路機能のどの部分をカバーしているかを定量的に評価する。等価性の判定において、等価性に関与している部分をのみを抽出する上で応用可能であることがわかった。
|
