表題番号：2002A-928 日付：2003/11/26
研究課題プログラムを仕様とするハードウェアの設計検証手法
研究者所属（当時） 資格 氏名
（代表者） 大学院情報生産システム研究科 教授 木村　晋二
研究成果概要
ハードウェアの設計の高位化に対応し、プログラムを仕様として用い、
ハードウェアの設計を形式的に検証する手法に関する研究を行った。まず、
現状の検証手法の調査を論文誌および国際会議、研究会などに対して
行った。その結果として、二分決定グラフを用いた厳密な順序回路の検証
手法、SAT に基づく近似的な検証手法、無評価関数に基づく等価性判定論理
の 3 つが基本的な手法であることと、これらを組み合わせたハードウェアの
検証手法の研究が盛んに行われていることがわかった。ただ、プログラムを
仕様とするものについては、プログラムの直接実行による、シミュレーションの
高速化の側面が主に強調され、形式的な手法の研究開発が不十分であることも
明らかとなった。
そこで、これらのハードウェアの手法の中で、大規模な回路に適用可能
と考えられる無評価関数に基づく等価性判定論理を適用した手法の開発を目指し、
そのための基礎的な研究を行った。無評価関数に基づく等価性判定論理では、
記号的な式の等価性を判断することができるので、プログラムの代入をそのまま
等価性判定の式に変換することで、二つのプログラムの等価性を式の等価性
として判定することができる。具体的には、Ｃ 言語のプログラムを対象と
して、それを等価性判定論理の式へ変換する規則を求めるとともに、多バイトの
演算問題に適用し、手法の有効性と適用限界を求めた。実際のプロセッサなど
で用いられている、桁上げ選択加算を含むような演算では、64 ビット程度の
加算の等価性の検証が時間的に不可能となることがわかり、等価性判定論理
自体の性質を含めて、今後のさらなる研究が必要である。