|
トランザクションレベルでの検証を行なうために、SMT (Satisfiability Modulo Theory)ソルバと呼ばれる形式的検証ツールの開発を行なった。SMTは命題論理の証明を行なうSAT (Satisfiability)ソルバと、1階述語論理のいくつかのTheoryの証明エンジンを組み合わせたもので、ここではハードウェアの検証に有効な、EUF (Equality with Uninterpreted Functions)とBV(Bit-Vectors)の証明エンジンを組み込んでいる。SATソルバは1年目の研究成果として開発したプログラムを用いている。大まかには、トップレベルの論題論理の構造を充足する解をSATソルバで求め、その部分解に対応する各々のTheoryが充足しているかを個々の証明エンジンで証明するというステップを実行する。証明を正しく行なうという意味ではすべての論理構造を一旦命題論理の形で表して、それをSATソルバで解けばよいが、その論理構造が充足不可能な場合の多くは、ごく一部の論理構造によって矛盾が起こっており、論理構造全体を命題論理の形で表す処理が非効率的である。そこで、論理構造を一旦AIG(AND-INVERTER-GRAPH)と呼ばれる2入力ANDゲートからなる論理回路の形式で表現し、AIGの構造に対して、論理最適化を行なうことで、簡単な矛盾の検出を行なうアルゴリズムの開発を行なった。局所的な矛盾はSATソルバを起動することなく検出することができるため、効率化に役立っている。
検証問題そのものは、命題論理に限定してもNP完全問題であり、どのような問題でも効率よく解けるという保障はないが、実用上は正しく設計できていることの自明な確認を形式的検証ツールを用いて保障させるという使い方が多いと思われるので、上記の工夫は有効である。
|
