| 研究課題/領域番号 |
05558030
|
|---|
| 研究種目 |
試験研究(B)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
矢島 修三 (矢島 脩三) 京都大学, 工学部, 教授 (20025901)
|
|---|
| 研究分担者 |
平石 裕実 京都産業大学, 工学部, 教授 (40093299)
荻野 博幸 京都大学, 工学部, 教務職員 (40144323)
武永 康彦 京都大学, 工学部, 助手 (20236491)
浜口 清治 (濱口 清治) 京都大学, 工学部, 講師 (80238055)
高木 直史 京都大学, 工学部, 助教授 (10171422)
|
|---|
| 研究期間 (年度) |
1993 – 1994
|
| 研究課題ステータス |
完了 (1994年度)
|
| 配分額 *注記 |
10,700千円 (直接経費: 10,700千円)
1994年度: 4,000千円 (直接経費: 4,000千円)
1993年度: 6,700千円 (直接経費: 6,700千円)
|
|---|
| キーワード | 時相論理 / 論理設計 / 形式的検証 / 論理関数処理 / 二分決定グラフ / モデルチェッキング / 仕様記述 / 論理開数処理 / 形式的論理設計検証 / 順序回路 |
|---|
| 研究概要 |
本研究では、時相論理に基づく論理設計の形式的検証システムについて、次の研究を行った。
(1)論理設計の形式的検証システムの試作
(a)従来形式的検証に用いられてきた分岐時間モデルに基づく時相論理に比べ、表現能力が高く、また直観的な記述が可能な線形時間時相論理を取り上げ、論理関数処理に基づく検証システムの開発・実装を行い、実例を検証し、その有効性を示した。(b)大規模回路を縮退するために開発した配列構造に基づく抽象化手法を実例に適用するには、部分回路の検証が必要であるが、従来法では、ビット数に対して指数時間の検証時間を要する乗算器が含まれているため、取り扱いが困難であった。本研究では、二分モーメントグラフと呼ばれるデータ構造を用いることで、乗算器について多項式時間での検証が可能であることを実験的に示すことに成功した。今後、配列構造に着目した抽象化手法と二分モーメントグラフに基づく手法を融合していくことが課題である。
(2)論理関数処理の高速化に関する研究
(a)二分決定グラフの処理について、論理演算、最小化の問題を取り上げ、その計算複雑度を確定した。(b)従来、論理関数処理に用いられて来た二分決定グラフの拡張とみなすことのできる、V節点を含む二分決定グラフや分岐プログラムの種々のクラスについてその表現能力を明らかにした。(c)二次記憶を用いて大規模な二分決定グラフを処理する手法を開発し、実装・実験を行ってその有効性を示した。
(3)システムのユーザインターフェースに関する研究
従来から開発してきたマルチスクリーン・マルチコンピュータシステムにXウィンドウ上での描画機能を実装し、二分決定グラフや論理回路図の描画を可能とした。
|
