2005 Fiscal Year Annual Research Report
類似度を考慮した等価論理を用いたハードウェアの高位設計検証手法の研究
| Project/Area Number |
17500047
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Waseda University |
|---|
Principal Investigator |
木村 晋二 早稲田大学, 大学院・情報生産システム研究科, 教授 (20183303)
|
|---|
| Keywords | 等価論理 / ハードウェアの等価検証 / 無評価関数 / 項書き換え |
|---|
| Research Abstract |
類似度を考慮した等価論理を用いたハードウェアの高位設計検証手法について、平成17年度は以下の研究を行った。
(1)現状手法に関しては、特にStanford大学で開発されたSVC(Stanford Validity Checker)およびCVC(Cooperating Validity Checker)についてアルゴリズムの調査を行った。
(2)ハードウェア記述言語Verilogおよびプログラミング言語Cによるハードウェア機能の記述を等価論理の式に変換するシステムの研究開発を行った。本システムは、Control Data Flow Graph (CDFG)を内部データフォーマットとして用い、Verilog記述の構文解析および意味解析を行ってCDFGを生成するモジュールと、C言語の構文解析および意味解析を行いCDFGを生成するモジュール、CDFGからCVCの式を生成するシステムからなる。現状では、入力として受け付けられる構文に制限があるものの、Verilog/CをCVC式に変換するシステムのプロトタイプを作成した。
(3)変数の類似度については、現状のCVC等のツールでは直接扱うことができないが、整数データについては不等式を記述することができ、変数を決めれば、差が1以下、2以下などと類似度を表すことができる。この類似度を用い、ループ構造を残したまま等価性比較をする手法を提案している。具体的には、ループの構造が異なるときに、中間結果の類似度をアンローリング回数で比較して、類似度が近くなるように交互にアンロールを行う手法である。
(4)等価検証に関連し、検証のカバレージ、浮動小数点演算の誤差解析手法、マルチスレッドプロセッサの検証、再構成可能ハードウェアの検証に関する研究を行った。
|
Research Products
(7 results)
