| 研究課題/領域番号 |
05558030
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
矢島 脩三 京都大学, 工学部, 教授 (20025901)
|
|---|
| 研究分担者 |
平石 裕実 京都産業大学, 工学部, 教授 (40093299)
荻野 博幸 京都大学, 工学部, 教務職員 (40144323)
武永 康彦 京都大学, 工学部, 助手 (20236491)
濱口 清治 京都大学, 工学部, 助手 (80238055)
高木 直史 京都大学, 工学部, 助教授 (10171422)
|
|---|
| キーワード | 形式的論理設計検証 / 時相論理 / 順序回路 / 論理関数処理 / 二分決定グラフ |
|---|
| 研究概要 |
実用的規模の回路を対象とする論理設計の形式的検証システムを実現するためには、検証手法および論理関数処理の両面で、より大規模な回路を扱うための手法の開発が重要である。この点に重点をおいて、「研究実施計画」に従い、主に以下の3項目について研究を進め、成果を得た。
(1)論理設計の形式的検証システムの試作 時相論理で記述された仕様に対して、検証すべき性質のみに着目することにより検証すべき順序回路の規模を縮退させる抽象化手法を開発した。特に配列型のデータ構造を含む順序回路の記述に対して、論理関数処理の利用を前提とした抽象化アルゴリズムを得た。また、パイプライン制御方式のマイクロプロセッサの形式的設計検証に関して、プロセッサを順序回路にモデル化し検証を行う手法を開発した。これらの手法を採り入れた設計検証システムの試作を進めている。
(2)論理関数処理の高速化に関する研究 二分決定グラフを用いた論理関数処理に関して、二次記憶を用いて大規模な二分決定グラフを効率良く処理する手法を開発し、その有効性を示した。また、二分決定グラフに基づく論理関数処理の基礎となる理論的な研究を行い、二分決定グラフの能力や処理の計算複雑さを明らかにした。
(3)システムのユーザ・インタフェースに関する研究 以前我々が開発したマルチコンピュータ・マルチスクリーン上に、大規模な二分決定グラフを表示する手法を開発した。
上記の研究成果を統合して、システムの試作を進めている。(2)の二分決定グラフの能力および処理の計算複雑さに関する研究成果を二編の論文にまとめ、論文誌に投稿し、採録が決定している。また、本試作研究の基礎となった研究成果の一部をまとめた二編の論文が論文誌に掲載された。
|
