1993 Fiscal Year Annual Research Report
時相論理に基づく論理設計の形式的検証システムの試作研究
| Project/Area Number |
05558030
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
矢島 脩三 京都大学, 工学部, 教授 (20025901)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
平石 裕実 京都産業大学, 工学部, 教授 (40093299)
荻野 博幸 京都大学, 工学部, 教務職員 (40144323)
武永 康彦 京都大学, 工学部, 助手 (20236491)
濱口 清治 京都大学, 工学部, 助手 (80238055)
高木 直史 京都大学, 工学部, 助教授 (10171422)
|
|---|
| Keywords | 形式的論理設計検証 / 時相論理 / 順序回路 / 論理関数処理 / 二分決定グラフ |
|---|
| Research Abstract |
実用的規模の回路を対象とする論理設計の形式的検証システムを実現するためには、検証手法および論理関数処理の両面で、より大規模な回路を扱うための手法の開発が重要である。この点に重点をおいて、「研究実施計画」に従い、主に以下の3項目について研究を進め、成果を得た。
(1)論理設計の形式的検証システムの試作 時相論理で記述された仕様に対して、検証すべき性質のみに着目することにより検証すべき順序回路の規模を縮退させる抽象化手法を開発した。特に配列型のデータ構造を含む順序回路の記述に対して、論理関数処理の利用を前提とした抽象化アルゴリズムを得た。また、パイプライン制御方式のマイクロプロセッサの形式的設計検証に関して、プロセッサを順序回路にモデル化し検証を行う手法を開発した。これらの手法を採り入れた設計検証システムの試作を進めている。
(2)論理関数処理の高速化に関する研究 二分決定グラフを用いた論理関数処理に関して、二次記憶を用いて大規模な二分決定グラフを効率良く処理する手法を開発し、その有効性を示した。また、二分決定グラフに基づく論理関数処理の基礎となる理論的な研究を行い、二分決定グラフの能力や処理の計算複雑さを明らかにした。
(3)システムのユーザ・インタフェースに関する研究 以前我々が開発したマルチコンピュータ・マルチスクリーン上に、大規模な二分決定グラフを表示する手法を開発した。
上記の研究成果を統合して、システムの試作を進めている。(2)の二分決定グラフの能力および処理の計算複雑さに関する研究成果を二編の論文にまとめ、論文誌に投稿し、採録が決定している。また、本試作研究の基礎となった研究成果の一部をまとめた二編の論文が論文誌に掲載された。
|
-
[Publications] 樋口博之,石浦菜岐佐,矢島脩三: "Compaction of Test Sets for Combinational Circuits Based on Symbolic Fault Simulation" 電子情報通信学会 英文論文誌. VOL,E76-D NO.9. 1121-1127 (1993)
-
[Publications] 樋口博之,濱口清治,矢島脩三: "Compact Test Sequences for Scan-Based Sequential Circuits" 電子情報通信学会 英文論文誌. VOL,E76-A NO.10. 1676-1683 (1993)
-
[Publications] 澤田宏,武永康彦,矢島脩三: "On the Computational Power of Binary Decision Diagrams" 電子情報通信学会 英文論文誌. 発表予定(採録決定).
-
[Publications] 武永康彦,矢島脩三: "Computational Complexity of Manipulating Binary Decision Diagrams" 電子情報通信学会 英文論文誌. 発表予定(採録決定).
