Research on Formal Verifier of Logic Design Based on Temporal Logic

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

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 systemWe implemented a new capability on Multi-Screen Multi-Window systems to enable drawings of binary decision diagrams or logic circuits.