1989 Fiscal Year Annual Research Report
正則時相論理に基づく形式的論理設計検証に関する研究
| Project/Area Number |
01550285
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
平石 裕実 京都大学, 工学部, 助教授 (40093299)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
荻野 博幸 京都大学, 工学部, 教務職員 (40144323)
石浦 菜岐佐 京都大学, 工学部, 助手 (60193265)
高木 直史 京都大学, 工学部, 助手 (10171422)
|
|---|
| Keywords | 時相論理 / 設計検証 / 論理設計 / 仕様記述 / 正則集合 / 順序機械 / 共有二分決定グラフ / 記号シミュレ-ション |
|---|
| Research Abstract |
正則時相論理に基づく形式的論理設計検証に関して、本年度は主として形式的論理設計検証システムを構築する際に必要となる基礎的な問題に対して研究を行い、以下の研究成果を得た。
1.正則時相論理に関する基礎的研究:既に我々が提案した正則時相論理は有限長時間のみを対象としていたが、無限長時間をも扱えてω正則集合と等価な表現能力を持つω正則時相論理の体系を明らかにし、また、階層的な設計検証法を示した。
2.論理設計検証アルゴリズムの研究:正則時相論理を用いた設計検証アルゴリズムとして、設計対象の順序機械の大きさに比例する時間で設計検証が可能な高率の良いモデルチェックアルゴリズムを示した。また、論理式の表現方法として共有二分決定グラフを提案し、これにより等価性や恒真性判定、記号シミュレ-ションなどの各種の論理式の処理が高率よく行えることを示した。
3.論理回路のモデル化とその仕様記述の研究:正則時相論理により数百状態の順序機械の入出力仕様の記述を行った。また、論理回路のモデルとして、非決定性順序機械によりモデル化を行うことにより、素子の遅延時間が一定でないような論理回路の記述が簡潔に行えることを示し、このモデルにより記述言語に対する形式的な意味付を行った。
4.設計検証評価システムの試作:
設計した順序機械が、正則時相論理式で記述された仕様を満たすかどうかをモデルチェック法により検証するシステムを実際に試作し、数百状態の順序機械に対して数分で検証が行えることが判明し、実用的な立場からも本手法が有効であることが明らかになった。
|
-
[Publications] Hiromi Hiraishi: "Design Verification of Sequential Machines Based on E-free Regular Temporal Logic" Proc.Computer Hardware Description Languages and Their Applications. 249-264 (1989)
-
[Publications] Nagisa Ishiura: "Time-Symbolic simulation for Accurate Timing Verification of Asynchrouous Behavior of Logic Circuits" Proc.26th ACM/IEEE Design Automation conference. 497-502 (1989)
-
[Publications] 浜口清治: "正則時相論理を用いた異なる階層間の設計検証について" 京都大学数理解析研究所構究録. 695. 253-262 (1989)
-
[Publications] Shin-ichi Minato: "Fast Tautology Cheching Using Shared Binary Decision Diagran-Benchmark Results-" Proc.IFIP International Work shop on Applied Formal Methods for Correct VLSI Dcsign. 580-584 (1989)
