1994 Fiscal Year Final Research Report Summary
Research on Formal Verifier of Logic Design Based on Temporal Logic
| Project/Area Number |
05558030
|
|---|
| Research Category |
Grant-in-Aid for Developmental Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | KYOTO UNIVERSITY |
|---|
Principal Investigator |
YAJIMA Shuzo Kyoto University, Faculty of Engineering, Professor, 工学部, 教授 (20025901)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
HIRAISHI Hiromi Kyoto Sangyo University, Faculty of Engineering, Professor, 工学部, 教授 (40093299)
OGINO Hiroyuki Kyoto University, Faculty of Engineering, Staff, 工学部, 教務職員 (40144323)
TAKENAGA Yasuhiko Kyoto University, Faculty of Engineering, Instructor, 工学部, 助手 (20236491)
HAMAGUCHI Kiyoharu Kyoto University, Faculty of Engineering, Lecturer, 工学部, 講師 (80238055)
|
|---|
| Project Period (FY) |
1993 – 1994
|
| Keywords | Temporal Logic / Logic Design / Formal Verification / Logic Function Manipulation / Binary Decision Diagram / Formal Specification / Model Checking |
|---|
| Research Abstract |
We studied the following topics on formal verifiers of logic designs based on temporal logic.
(1) Formal verifier of logic designs
(a) Temporal logics based on linear models are much more expressive and succinct in describing specifications. We implemented a verification algorithm based on logic function manipulation and showed its effectiveness for practical examples. (b) We developed a abstraction technique based on array structures in large logic circuits. In order to apply this technique to large examples, we needed to develop a method for verifying circuits, such as multipliers, which were intractable with known techniques. Using binary moment diagrams, we developed a new method, and showed through experiments that we can handle multipliers in polynomial time. We are dealing with incorporating the above two methods.
(2) High-speed manipulation of logic functions.
(a) We clarified the computational complexity of Boolean operations and minimization problems over binary decision diagrams. (b) We extended the binary decision diagrams to allow V-nodes, and showed its expressive power. We also investigated the expressive powers of various branching programs. (c) We developed a new method for handling extremely large binary decision diagrams on secondary storages. We showed its effectiveness through experiments.
(3) User interface of the system
We implemented a new capability on Multi-Screen Multi-Window systems to enable drawings of binary decision diagrams or logic circuits.
|
