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)
平石 裕実 京都産業大学, 工学部, 教授 (40093299)
|
|---|
| Project Period (FY) |
1995 – 1996
|
| Project Status |
Completed (Fiscal Year 1996)
|
| Budget Amount *help |
¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 1996: ¥2,200,000 (Direct Cost: ¥2,200,000)
|
|---|
| 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.
|
Report
(3 results)
Research Products
(5 results)
