1991 Fiscal Year Annual Research Report
ブ-ル関数処理による順序回路の自動合成・設計検証システムの試作研究
Project/Area Number |
03555074
|
Research Institution | Kyoto University |
Principal Investigator |
矢島 脩三 京都大学, 工学部, 教授 (20025901)
|
Co-Investigator(Kenkyū-buntansha) |
平石 裕実 京都産業大学, 工学部, 教授 (40093299)
荻野 博幸 京都大学, 工学部, 教務職員 (40144323)
武永 康彦 京都大学, 工学部, 助手 (20236491)
高木 直史 京都大学, 工学部, 助教授 (10171422)
|
Keywords | 論理合成 / 論理設計検証 / 順序回路 / 論理関数簡単化 / 状態割当て / 時相論理 / 論理設計支援 |
Research Abstract |
ブ-ル関数処理による順序回路の自動合成・設計検証システムの試作研究に関して、以下の成果を得た。 1.順序回路の状態割当法、論理関数簡単化に関する研究 順序回路の状態割り当てアルゴリズムとして、一発状態割当てアルゴリズムを提案し、これに基づいたシステムの試作にとりかかった。また、順序回路の自動合成の基礎である組合せ回路の最適化問題についても研究を行ない、ブ-ル関数処理を利用した効率的な手法を提案した。 2.ブ-ル関数処理アルゴリズムに関する研究 ブ-ル関数処理のために用いられる共有二分決定グラフの性質について研究を行ない、同グラフを用いた論理演算の並列処理について、その計算量を明らかにした。 3.システムのユ-ザ・インタフェ-スに関する研究 開発したプログラムを結合した際のユ-ザ・インタフェ-スの充実の観点から、複数のワ-クステ-ションを利用した高解像度大画面の実現について研究し、これに基づいて描画用ライブラリを試作、実験を行なった。 4.順序回路の設計検証アルゴリズムの研究 分岐時間正則時相論理を仕様記述言語とする順序回路の設計検証について、ブ-ル関数処理を利用したアルゴリズムを提案し、これに基づく順序回路の検証システムを試作した。同システム上で実験を行なった結果、従来手法では検証不可能だった規模の回路を取り扱いうることが明らかとなり、現在、より大規模な回路を取り扱うための検証手法について検討を進めている。
|
Research Products
(4 results)
-
[Publications] H.Ochi: "Breadth-First Manipulation of SBDD of Boolean Functions for Vector Processing" Proceedings of the 28th ACM/IEEE Design Automation Conference. 413-416 (1991)
-
[Publications] H.Hiraishi: "Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification" Proceedings of the 3rd Workshop on Computer-Aided Verification. 1. 279-290 (1991)
-
[Publications] K.Hamaguchi: "Formal Verification of Speed-Dependent Asynchronous Circuits Using Symbolic Model Checking of Branching Time Regular Temporal Logic" Proceedings of the 3rd Workshop on Computer-Aided Verification. 2. 478-488 (1991)
-
[Publications] 濱口 清治: "形式的設計検証のための分岐時間正則時相論理" 情報処理学会論文誌. 33. (1992)