マイクロプロセッサの形式的論理設計検証システムの試作研究

1996 Fiscal Year Annual Research Report

• Project/Area Number: 07558155
• Research Institution: KYOTO UNIVERSITY
• Principal Investigator: 矢島 脩三 京都大学, 工学研究科, 教授 (20025901)
• Co-Investigator(Kenkyū-buntansha): 荻野 博幸 京都大学, 工学研究科, 助手 (40144323) ; 武永 康彦 京都大学, 工学研究科, 助手 (20236491) ; 浜口 清治 大阪大学, 基礎工学部, 講師 (80238055)
• Keywords: 形式的設計検証 / 機能レベル設計 / 時相論理 / 第一階述語論理 / モデルチェッキング / 論理関数処理 / 二分決定グラフ

Research Abstract

本研究では、大規模な順序回路設計の中でも、特にマイクロプロセッサの正しさを厳密に保証するための形式的検証システムの試作を目指している。本研究では本年度の研究の準備として、前年度に二分モーメントグラフを用いて、マイクロプロセッサで重要な構成要素となっている算術演算回路、特に乗算器に対するきわめて効率の良いアルゴリズムを構築・実装し、また、時間に関する性質について、より直観的な記述が可能な線形時間時相論理による設計検証アルゴリズムを実装したほか、ゲートレベルではなくデータパスなどを抽象化した機能レベルの記述を直接検証するために、限量子を含まない等号付第一階述語論理の恒真性判定問題の効率の良いアルゴリズムについて検討した。さらに設計検証において基盤技術となる二分決定グラフによる論理関数処理について、その変数順序付け問題がNP完全となるとを示した。これを踏まえて今年度は、限量子を含まない等号付第一階述語論理に、上記の線形時間時相論理に類似した時相演算子を導入し、時間に関する性質の直観的な記述が容易な体系を構築した。この論理について、まず、設計検証に用いる恒真判定問題が決定可能であることを証明し、人手による介入を必要しない自動的な検証システムの構築が可能であることを示した。次にこのアルゴリズムを時間および領域量の点から改良して実装し、その有効性を示した。また。設計検証において基盤技術となっている二分決定グラフについて、OR節点と呼ばれる特殊な節点を導入した場合の、二分決定グラフの表現能力について研究を行った。