Research on Development of Formal Logic Design Verifier for Microprocessors
Project/Area Number  07558155 
Research Category 
GrantinAid for Scientific Research (A)

Section  試験 
Research Field 
計算機科学

Research Institution  KYOTO UNIVERSITY 
Principal Investigator 
YAJIMA Shuzo Kyoto University, Guraduate School of Engineering, Professor, 工学研究科, 教授 (20025901)

CoInvestigator(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 Fiscal Year 
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 / Firstorder 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 quantifierfree firstorder 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 NPcomplete. We also investigated the computational power of a variant binary decision diagrams which have nondeterministic nodes.

Report
(4results)
Research Output
(5results)