| 研究概要 |
近年のハードウェア設計では,設計検証に要する時間が増加しつづけ,全設計工程の60%--80%もの時間を占めるようになっている.これに対して,フォーマル検証の適用が始まっているが、これらの多くはレジスタ転送レベルやゲートレベルより高位の設計には適用できない.本研究では、C言語などで書かれた高位のハードウェア記述に対して,2つの記述の機能の等価性判定を行う手法を研究する.具体的には,記述中にあらわれる算術演算を,第1階述語論理における関数記号によって表現し,意味を解釈せずに記号のまま処理することにより,効率化を図る.
しかしながら,この手法では,2つの記述が極めて似通っていなければ等価と判定することができない.これを解決するため,本年度は,まず,同値制約のもとでの等価性判定アルゴリズムの検討と実装を行った.この同値制約は,たとえば,2つの記述に対して,(x>1⇔x-1>0)といった形で与えられ,記述内に出現する部分式で左辺のパターンに合致するものと右辺のパターンに合致するものがあれば,等価と見なすというものである.この結果、parcorフィルタなど信号処理プログラムについて、ループ部分を数千回にわたって展開した記述2つの等価性判定を、数千秒でできることが明らかとなった.
一方,必要な同値制約を与えることが難しい場合や,2つの記述が極端に異なる場合,意味を解釈しないで処理する方法ではうまく等価性判定ができない.これに対して一時的に算術演算記号にブール関数レベルでの解釈を与えて評価し判定の精度をあげる方法が考えられる.本年度は、高位レベルでの検証の際に得られる反例について、ブール関数レベルでの再チェックを行うアルゴリズムを実装し、精度を高めた判定が可能であることを同じく信号処理プログラムを対象として示した。こうして得られた等価関係を,同値制約として以降の処理に再利用する手法については、今後検討していく予定である。
|
