研究課題/領域番号 |
05558030
|
研究機関 | 京都大学 |
研究代表者 |
矢島 脩三 京都大学, 工学部, 教授 (20025901)
|
研究分担者 |
平石 裕実 京都産業大学, 工学部, 教授 (40093299)
荻野 博幸 京都大学, 工学部, 教務職員 (40144323)
武永 康彦 京都大学, 工学部, 助手 (20236491)
浜口 清治 京都大学, 工学部, 講師 (80238055)
|
キーワード | 時相論理 / 論理設計 / 形式的検証 / 論理開数処理 / 二分決定グラフ / モデルチェッキング / 仕様記述 |
研究概要 |
交付申請書に記載の通り、平成5年度に引続き、次の研究を行った。 (1)論理設計の型式的検証システムの試作 (a)仕様記述能力の改善:従来形式的検証に用いられてきた分岐時間モデルに基づく時相論理に比べ表現能力が高く、また直観的な記述が可能な線形時間時相論理を取り上げ、論理関数処理に基づく検証アルゴリズムの開発・実装を行い、実例を検証し、その有効性を示した。(b)対象の抽象化:大規模回路中の部分回路を抽象化するためには、部分回路ごとの検証がまず必要となるが、マイクロプロセッサなどでは、従来法を適用すると、ビット数に対して指数時間の検証時間を要する乗算器などが部分回路として含まれているため、問題となっていた。本研究では、二分モーメントグラフと呼ばれるデータ構造を用いることで、多項式時間での検証が可能であることを実験的に示すことに成功した。また、配列構造に着目した抽象化手法を開発しており、今後これらを融合していくことが課題となっている。 (2)論理関数処理の高速化に関する研究 (a)二分決定グラフの種々の拡張:従来、論理関数処理に用いられて来た二分決定グラフの拡張とみなすことのできる、V節点を含む二分決定グラフや分岐プログラムの種々のクラスについてその表現能力を明らかにした。(b)大規模な二分決定グラフの処理技法:二次記憶を用いて大規模な二分決定グラフを処理する手法を開発し、実装・実験を行ってその有効性を示した。 (3)システムのユーザインターフェースに関する研究 従来から開発してきたマルチスクリーン・マルチコンピュータシステムにXウィンドウ上での描画機能を実装し、二分決定グラフや論理回路図の描画を可能とした。
|