|
本年度は正則時相論理やCTLをベ-スにして、計算機援用形式的設計検証システムを構築する際に必要となる基礎的な問題に関して研究を進め、主として以下の研究成果が得られた。
1.時相論理に関する基礎的研究:CTLより真に表現能力が高く有限状態システムの仕様を記述できる表現能力を持ちしかも検証対象の論理システムの大きさに比例する時間で効率良く検証が行なえる分岐時間正則時相論理BRTLの体系を明かにし、その効率的な記号モデル検査アルゴリズムを示した。
2.形式的設計検証アルゴリズムの研究:CTLとBRTLについて、効率的な論理関数処理が可能な共有二分決定グラフSBDDを用いた記号モデル検査アルゴリズムを示し、実際な実用規模の論理回路の設計検証に適用しそれらの有効性を示した。また、SBDDの処理アルゴリズムとして、ベクトル計算機に適したベクトルアルゴリズムを示し、約20倍程度のベクトル加速率を達成した。さらに、SBDDでは変数の順序付けによりその大きさが大幅に変化するため、(準)最適な変数の順序付けを求めるアルゴリズムを示した。
3.論理システムの仕様記述と検証:実用規模の論理システムとして、パイプライン方式のALUの完全な仕様記述を行ないCTLのベクトル記号モデル検査アルゴリズムを用いて設計検証を行なった。さらに、より大規模な論理システムとして8ビットマイクロプロセッサ(KUEチップ)の仕様記述を行ない、BRTLの記号モデル検査アルゴリズムを用いてその設計検証を行ないつつある。これらの実用規模の論理システムの設計検証を通して、我々の手法が十分実用化に耐えるものであることが判明した。
|
