1991 Fiscal Year Annual Research Report
時相論理に基づく計算機援用形式的設計検証に関する研究
| Project/Area Number |
03650301
|
|---|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
平石 裕実 京都産業大学, 工学部, 教授 (40093299)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
石浦 菜岐佐 大阪大学, 工学部, 講師 (60193265)
|
|---|
| Keywords | 論理設計検証 / 形式的検証 / 時相論理 / 計算機援用設計 / ベクトル計算機 |
|---|
| Research Abstract |
本年度は正則時相論理やCTLをベ-スにして、計算機援用形式的設計検証システムを構築する際に必要となる基礎的な問題に関して研究を進め、主として以下の研究成果が得られた。
1.時相論理に関する基礎的研究:CTLより真に表現能力が高く有限状態システムの仕様を記述できる表現能力を持ちしかも検証対象の論理システムの大きさに比例する時間で効率良く検証が行なえる分岐時間正則時相論理BRTLの体系を明かにし、その効率的な記号モデル検査アルゴリズムを示した。
2.形式的設計検証アルゴリズムの研究:CTLとBRTLについて、効率的な論理関数処理が可能な共有二分決定グラフSBDDを用いた記号モデル検査アルゴリズムを示し、実際な実用規模の論理回路の設計検証に適用しそれらの有効性を示した。また、SBDDの処理アルゴリズムとして、ベクトル計算機に適したベクトルアルゴリズムを示し、約20倍程度のベクトル加速率を達成した。さらに、SBDDでは変数の順序付けによりその大きさが大幅に変化するため、(準)最適な変数の順序付けを求めるアルゴリズムを示した。
3.論理システムの仕様記述と検証:実用規模の論理システムとして、パイプライン方式のALUの完全な仕様記述を行ないCTLのベクトル記号モデル検査アルゴリズムを用いて設計検証を行なった。さらに、より大規模な論理システムとして8ビットマイクロプロセッサ(KUEチップ)の仕様記述を行ない、BRTLの記号モデル検査アルゴリズムを用いてその設計検証を行ないつつある。これらの実用規模の論理システムの設計検証を通して、我々の手法が十分実用化に耐えるものであることが判明した。
|
-
[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] H.Ochi: "A Vector Algorithm for Manipulating Boolean Functions Based on Shared Binary Decision Diagrams" Proceedings of the International Symposium on Supercomputing. 191-200 (1991)
-
[Publications] N.Isihura: "Minimization of Binary Decision Diagrams Based on Exchanges of Variables" Proceedings of the IEEE International Conference on computer-Aided Design(ICCAD-91). 472-475 (1991)
