1996 Fiscal Year Final Research Report Summary
Research on Development of Formal Logic Design Verifier for Microprocessors
| Project/Area Number |
07558155
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (A)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 試験 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | KYOTO UNIVERSITY |
|---|
Principal Investigator |
YAJIMA Shuzo Kyoto University, Guraduate School of Engineering, Professor, 工学研究科, 教授 (20025901)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
OGINO Hiroyuki Kyoto University, Guraduate School of Engineering, Instructor, 工学研究科, 助手 (40144323)
TAKENAGA Yasuhiko Kyoto University, Guraduate School of Engineering, Instructor, 工学研究科, 助手 (20236491)
HAMAGUCHI Kiyoharu Osaka University, Feculty of Engineering Science, Lecturer, 基礎工学部, 講師 (80238055)
|
|---|
| Project Period (FY) |
1995 – 1996
|
| Keywords | Formal design verification / Function level design / temporal logic / First-order Predicate logic / model checking / logic function manipulation / binary decision diagram |
|---|
| Research Abstract |
The aim of this research is to develop a formal verifier for large sequential circuits, in particular, microprocessors. Although arithmetic circuits such as multipliers are crucial components in microprocessor designs, it was a hard problem to verify them. We developed a new algorithm using binary moment diagrams, and showed that it is possible to verify multipliers, which were typical hard problems in formal verification. Furthermore, we developed a new efficient algorithm for formal verification based on linear time temporal logic, which can describe temporal properties more easily than the other temporal logics. In order to deal with circuits at function level than at logic level, we took a logic known as quantifier-free first-order predicate logic with equality. We introduced temporal operators similar to those of the above linear time temporal logic, and proved that its validity checking problem is decidable. We improved this algorithm in terms of required time and space, and implemented the algorithm to show its effectiveness. Furthermore we showed that the optimal variable ordering problem of binary decision diagrams is NP-complete. We also investigated the computational power of a variant binary decision diagrams which have nondeterministic nodes.
|
Research Products
(2 results)
