2005 Fiscal Year Annual Research Report
高位ハードウェア設計記述に対する等価性判定手法の研究
| Project/Area Number |
16500030
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
浜口 清治 大阪大学, 大学院・情報科学研究科, 助教授 (80238055)
|
|---|
| Keywords | フォーマル検証 / 第一階述語論理 / 高位ハードウェア検証 / 充足可能性判定 |
|---|
| Research Abstract |
近年のハードウェア設計では,全設計工程中で設計検証の占める割合が増大し,60%--80%もの時間を要するようになっている.この問題に対処するべく,フォーマル検証の適用が始まっているが、フォーマル検証の手法の多くはレジスタ転送レベルやゲートレベルより高位の設計には適用できない.本研究では、C言語などで書かれた高位のハードウェア記述に対して,2つの記述の機能の等価性判定を行う手法を研究している.具体的には,記述中にあらわれる算術演算や機能ブロックを,第1階述語論理における関数記号や述語記号によって表現し,意味を解釈せずに記号のまま処理することにより,効率化を図る.
この手法の問題は,2つの記述が極めて似通っていなければ等価と判定することができないという点である.これを補うため,本研究では,同値制約のもとでの等価性判定アルゴリズムの検討と実装を行ってきている.この同値制約は,(x>1⇔x-1>0)といった形の規則であり,等価とみなすべきパターンを与えるために用いる.本年度は昨年度実装したプログラムに対して,コンフリクト解析と呼ばれる手法を付加した。これにより,parcorフィルタなど信号処理プログラムについて、ループ部分を数千回にわたって展開した記述同士の等価性判定が約10倍高速化し,数百秒でできることを確認した.
また,必要な同値制約を与えることが難しい場合や,2つの記述が大きく異なる場合は,意味を解釈しないで処理する方法ではうまく等価性判定ができない.これに対して,算術演算記号や機能ブロックにブール関数レベルでの解釈を与えて評価し,判定の精度をあげる方法の適用を試みてきている.昨年度は,高位レベルでの検証の際に得られる反例について、ブール関数レベルでの再チェックを行うアルゴリズムを実装したが,本年度はこれをさらに改良し、ブール関数レベルでの再チェック部分を削減するヒューリスティクを開発/実装した.これにより,同じく信号処理プログラムについて,昨年度のプログラムに比べ,約10倍程度高速に実行できることを確認した.
以上2つのプログラムを組み合わせ,より大きな問題に対して適用していくことが,来年度の課題である.
|
Research Products
(1 results)
