Research on Formal Verifier of Logic Design Based on Temporal Logic

我们对基于时态逻辑的逻辑设计的形式化验证器进行了以下研究：(1)逻辑设计的形式化验证器(A)基于线性模型的时态逻辑在描述规范方面更具表现力和简明性。实现了一种基于逻辑函数操作的验证算法，并通过实例验证了该算法的有效性。(B)在大型逻辑电路中提出了一种基于数组结构的抽象技术。为了将这项技术应用到大型例子中，我们需要开发一种方法来验证电路，例如乘法器，这是已知技术难以解决的。利用二进制矩图，我们提出了一种新的方法，并通过实验表明，我们可以在多项式时间内处理乘法器。我们正在处理结合上述两种方法。(2)逻辑函数的高速操作。(A)我们阐明了布尔运算的计算复杂性和二元决策图上的最小化问题。(B)对二叉决策图进行了扩展，使其支持V-节点，并展示了它的表达能力。我们还调查了各种分支程序的表达能力。(C)我们开发了一种新的方法来处理二级存储上的超大二叉决策图。系统的用户界面我们在多屏幕多窗口系统上实现了一种新的功能，可以绘制二元判决图或逻辑电路。

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.