時相理論を用いた形式的論理設計検証に関する研究

点击翻译按钮获取中文摘要

本年度は、主として時空間様相論理と並列検証アルゴリズムの基礎的研究を行なった。1.時空間様相論理の基礎的研究: 同一の回路を一次元的に繰り返し接続するビットスライス的な回路の設計検証において、回路の動作を、時間方向と空間方向の2つの遷移関係を持つ時空間Kripke構造としてモデル化する方法を提案した。これにより、任意長のビット幅を持つビットスライスALU回路などをコンパクトにモデル化出来る。また、この時空間Kripke構造に対する仕様記述のために、時間方向と空間方向の変化を記述できる時空間様相理論体系を示した。そらに、検証アルゴリズムとして、時空間様相論理の記号モデル検査アルゴリズムを示し、実際に簡単なALUの設計検証に適用し、本検証手法が有効であることを示した。2.並列検証アルゴリズムの基礎的研究: 現在、CPUの個数が数個から十数個程度の高性能ワークステーションが比較的安価に入手可能となってきている。そこで、このようなワークステーション上での実行に適した並列検証アルゴリズムの研究を行なった。とくに、設計検証で用いる記号モデル検査アルゴリズムの中心的な役割を担う共有二分決定グラフ(BDD)による論理関数処理の並列化を行なうために、BDD演算のマルチレッドアルゴリズムを開発した。このマルチスレッドアルゴリズムでは、並列処理の正当性を確保するために、内部の節点テーブルや演算結果テーブルのアクセスの際にロックをかける必要があるが、ロックの方法やロックをかける範囲が効率に大きな影響を及ぼすことが判明し、今後引続き研究を進める必要がある。