Research on Formal Verifier of Logic Design Based on Temporal Logic

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

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.