大規模論理設計の形式的検証に関する研究

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

本年度は、主として時空間様相論理の並列検証アルゴリズムの基礎的研究と、具体的な設計検証問題として耐故障設計の形式的検証を行なった。1.時空間様相論理の並列検証アルゴリズム:時空間様相論理の検証アルゴリズムでは、時間方向と空間方向の逆像計算が中心になる。これらの逆像計算の並列アルゴリズムとして、CPUの個数が数個から十数個程度の高性能ワークステーション上での実行に適したアルゴリズムと、50台程度のワークステーションを高速ネットワークで結合した分散システム上での実行に適したアルゴリズムの基礎的研究を行なった。前者では、マルチスレッドに基づく並列アルゴリズムを種々検討し、後者では、各ワークステーションで共有すべきデータの管理手法を種々検討した。その結果、並列処理の正当性を確保するために、種々の共有データへのアクセスの際にロックをかける必要があるが、ロックの方法やキャッシュの方法が効率に大きな影響を及ぼすことが判明した。今後引続き研究を進める必要があると考えられる。2.耐故障設計の形式的検証:論理回路の耐故障設計では、設計した回路がセルフテスト性やセルフチェック性を持つことが要求される場合が多い。これらの性質は回路内部に故障を仮定した上で満たされるべき性質であり、その検証は煩雑になる。そこで、これらの性質を論理関数で表現し、論理関数処理でこれらの性質の検証を行うアルゴリズムを示し、実際に論理シミュレーションによる検証に比べて数倍高速に検証できることを示した。