1992 Fiscal Year Annual Research Report
ブール関数処理による順序回路の自動合成・設計検証システムの試作研究
| Project/Area Number |
03555074
|
|---|
| Research Institution | KYOTO UNIVERSITY |
|---|
Principal Investigator |
矢島 脩三 京都大学, 工学部, 教授 (20025901)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
平石 裕実 京都産業大学, 工学部, 教授 (40093299)
荻野 博幸 京都大学, 工学部, 教務職員 (40144323)
武永 康彦 京都大学, 工学部, 助手 (20236491)
濱口 清治 京都大学, 工学部, 助手 (80238055)
高木 直史 京都大学, 工学部, 助教授 (10171422)
|
|---|
| Keywords | 論理合成 / 論理設計検証 / 順序回路 / 論理関数簡単化 / 状態割当て / 時相論理 / 論理設計支援 |
|---|
| Research Abstract |
平成3年度の成果をもとにさらに研究を進め、以下のように、自動合成・設計検証システムの試作を行った。
1.ブール関数処理による順序回路の自動合成システムの試作
前年度提案したブール関数処理を利用した単発状態割り当てアルゴリズムを計算機上に実現し、評価を行った。また、STT(single transition time)状態割り当てについても符号ベクトル長最小の状態割り当てを求めるブール関数処理に基づくアルゴリズムを構築・計算機上に実現した。
2.ブール関数処理による順序回路の設計検証システムの試作
前年度に試作したブール関数処理を利用した設計検証システムのプロトタイプで得られた結果をもとに、さらに設計検証アルゴリズムの改良を進め、マイクロプロセッサKUE-CHIP2などの検証に適用したところ、5-10倍の高速化が達成され、また、これまで記憶領域不足で検証不可能であった性質も検証可能となった。
3.ブール関数処理の効率的処理手法
共有二分決定グラフによるブール関数処理について、新たにグラフが小さくなる入力変数の順序づけを求める手法および巨大な共有二分決定グラフを扱うため2次記憶を利用するアルゴリズムを考案・実現した。
4.自動合成・設計検証システムのグラフィク・インタフェース
前年度に作成したマルチコンピュータ・マルチスクリーン(MCMS)・システム用ライブラリを利用し、ワークステーション上にXウィンドウ環境のもとでMCMSシステムを実現し、自動合成・設計検証システムのインタフェースのための高解像度と高速描画を達成した。
|
Research Products
(6 results)
-
[Publications] 濱口 清治: "形式的設計検証のための分岐時間正則時相論理" 情報処理学会論文誌. 33. 405-414 (1992)
-
[Publications] K.Hamaguchi: "∞-Regular Temporal Logic and its Model Checking Problem" Theoretical Computer Science. 103. 191-204 (1992)
-
[Publications] K.Hamaguchi: "Formal Design Verification of Seguential Machines Basedon Symbolic Moclel Checking for Branching Time Regular Tempoial Logic" IEICE Trans.Fundamentals. E75-A. 1220-1229 (1992)
-
[Publications] N.Ishiura: "Coded Time-Symbolic Simulation for Timing Verification of Logic Circuits" IEICE Trans.Fundamentals. E75-A. 1247-1254 (1992)
-
[Publications] H.Higuchi: "Compaction of Test Sets Based on Symbolic Fault Simulation" Proceedings of the Synthesis and Simulation Meeting and International Intercharge. 253-262 (1992)
-
[Publications] K.Hamaguchi: "Design Verification of Asynchronous Sequential Circuits Using Symbolic Model Checking" Proceedings of International Symposium on Logic Synthesis and Microprocessor Architecture. 84-90 (1992)
