| 研究概要 |
近年のハードウェア設計では,全設計工程中で設計検証の占める割合が増大し,60%-80%もの時間を要するようになっている.この問題を緩和するための一手法として,フォーマル検証の適用が始まっているが、フォーマル検証の手法の多くは,計算量の点で,レジスタ転送レベルやゲートレベルより高位の設計に直接的には適用できない.本研究では、C言語などで書かれた高位のハードウェア記述に対して,2つの記述の機能の等価性判定を行う手法を研究している.具体的には,記述中にあらわれる算術演算や機能ブロックを,第1階述語論理における関数記号や述語記号によって表現し,意味を解釈せずに記号のまま処理することにより,効率化を図る.
この手法の問題は,2つの記述が極めて似通っていなければ等価と判定することができないという点である.これを補うため,本研究では,同値制約のもとでの等価性判定アルゴリズムの検討と実装を行ってきている.この同値制約は,(x>1⇔x-1>0)といった形の規則であり,等価とみなすべきパターンを与えるために用いる.本年度は昨年度に引き続き,コンフリクト解析と呼ばれる手法の改良を行うと同時に,同値制約の処理の拡張を行って,これまで本研究の枠組みでは取り扱うことができなかった結合法則なども扱う事も可能とした.
前年度までに開発してきたプログラムに,上記のような改良を加えることにより,より大きな規模の設計に対する実験が可能となり,PARCORフィルタ,ADPCMフィルタ,フーリエ変換処理,平方根計算のプログラムに対する等価性判定に適用を試みた.その結果,加算減算のみで構成された設計の場合には,従来のブール函数レベルでの等価性判定手法の方が有効であるが,乗算等より複雑な演算(非線形の演算)を含む場合には,本研究のアプローチにより,1-2桁程度高速,あるいは従来の手法では計算量的に判定困難であるような規模でも判定が可能となった.
|
