| 研究課題/領域番号 |
07558155
|
|---|
| 研究種目 |
基盤研究(A)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 試験 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
矢島 脩三 京都大学, 工学研究科, 教授 (20025901)
|
|---|
| 研究分担者 |
荻野 博幸 大阪大学, 工学研究科, 助手 (40144323)
武永 康彦 京都大学, 工学研究科, 助手 (20236491)
浜口 清治 大阪大学, 基礎工学部, 講師 (80238055)
平石 裕実 京都産業大学, 工学部, 教授 (40093299)
|
|---|
| 研究期間 (年度) |
1995 – 1996
|
| 研究課題ステータス |
完了 (1996年度)
|
| 配分額 *注記 |
2,200千円 (直接経費: 2,200千円)
1996年度: 2,200千円 (直接経費: 2,200千円)
|
|---|
| キーワード | 形式的設計検証 / 機能レベル設計 / 時相論理 / 第一階述語論理 / モデルチェッキング / 論理関数処理 / 二分決定グラフ / マイクロプロセッサ / 調理関数処理 / 二分モーメントグラフ / 三分決定グラフ / 機能レベル検証 / 算術演算回路検証 |
|---|
| 研究概要 |
本研究では、大規模な順序回路設計の中でも、特にマイクロプロセッサの正しさを厳密に保証するための形式的検証システムの試作を目指している。算術演算回路はマイクロプロセッサの重要な構成要素のひとつであるが、特に乗算器などの算術演算回路を検証することは一般に難しかった。これに対して、本研究では二分モーメントグラフによる新しいアルゴリズムを開発・実装して、従来手法では扱いきれなかった乗算器の検証が、現実的な時間で検証可能であることを世界で初めて示した。また、より直観的な記述が可能な時相論理である線形時間型の論理LTL (Linear Time Temporal Logic)に対して、従来より効率的な検証アルゴリズムを構築・実装して、有効性を示した。一方、マイクロプロセッサのような回路の設計検証を、論理回路レベルで直接行うことは、あまり現実的とはいえない。そこで本研究では、データパスなどを抽象化するために、限量子のない等号付き第一階述語論理を取り上げて、上記の線形時間型の時相論理に類似した時相演算子を導入し、時間に関する性質の直観的な記述が容易な体系を構築した。この論理について、まず、設計検証に用いる恒真判定問題が決定可能であることを証明した。次にこのアルゴリズムを時間および領域量の点から改良して実装し、その有効性を示した。また、設計検証において基盤技術となっている二分決定グラフについて、その変数順序付け問題がNP完全であることや、OR節点と呼ばれる特殊な節点を導入した場合の、二分決定グラフの表現能力について研究を行った。
|
