Research on Development of Formal Logic Design Verifier for Microprocessors

点击翻译按钮获取中文摘要

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.