|
本研究は、形式的な設計検証のための基礎的な手法の確立を目的として、時間の概念を陽に記述することが出来る時相論理を用いて有限状態機械の形式的設計検証の研究を行い、以下の成果を得た。
1.分岐時間正則時相論理: 効率の良い検証アルゴリズムの存在が示されている時相論理CTLに比べて、真に表現能力が高くしかも検証アルゴリズムの複雑さはCTLと同等の分岐時間正則時相論理BRTLを提案し、その検証アルゴリズムとして効率の良い記号モデル検査アルゴリズムを示した。実際にBRTLを用いた形式的設計検証システムを試作し、8ビットマイクロプロセッサの検証に適用してその有効性を示した。
2.形式的検証アルゴリズム: 記号モデル検査法では論理関数を二分決定グラフ(BDD)を用いて表現し、BDDを処理することにより検証を行うが、BDD処理を高速化するためにベクトル計算機向きのBDD処理アルゴリズムを提案し、これにより20倍程度のベクトル加速率が得られることを示した。また、BRTLやCTLの記号モデル検査アルゴリズムの基本演算である逆像計算のBDD処理向きの効率の良いアルゴリズムを示し、従来の方法に比べて8〜40倍程度高速化出来ることを示した。
3.実用規模の論理システムの検証: BRTLを用いて8ビットマイクロプロセッサ(KUEチップ)の検証を行い、設計誤りを発見するとともにそれ以外の部分については設計が正しいことを示した。この検証においてはKUEチップの内部メモリをメモリに対する入出力命令として抽象化することが有効であると判明した。また、CTLを用いて、マルチマイクロプロセッサ用のバス(Futureバス)のキャッシュコヒレンシープロトコルの検証を行い、共有メモリやキャッシュを1ビットメモリとして抽象化できることを示した。
|
