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