Research on formal verification of asynchronous logic circuits with bounded delays

异步电路通常采用与速度无关的模型建模，其中门的延迟是无界的或有一个未知常数的限制。大部分的研究都是关于设计的。合成。并在此模型下对异步电路进行了验证。尽管与速度无关的模型非常简单。无界延迟的可能性有时迫使设计者给电路增加额外的复杂性。最近。为了设计快速、紧凑的异步电路，通常采用有界延迟模型。然而。这些定时异步电路不能再使用非定时验证算法进行精确验证。因此。在本研究中，我们的目标是建立一个能恰当表达这些定时电路的定时模型。在第一年，我们从理论上形式化了基于时间跟踪理论的验证方法，并证明了使用时间Petri网实现验证方法的正确性。然后，我们尝试将在不影响正确性的前提下只遍历后继状态子集的偏序约简技术应用于时间验证方法。通过样机的实验结果，验证了该方法的有效性。第二年。在理论部分，我们提出了基于时间跟踪理论的几种正确性定义，并推导了验证正确性算法可实现的充分条件。进一步。我们证明了去年提出的偏序约简算法的正确性。对于实际的部分。我们实现了基于偏阶约简的第二版验证算法。利用该方法可以比以往的方法更有效地验证各种定时异步电路。此外，为了减少验证方法中的内存使用，我们提出了共享技术。压缩。细化访问过的州的信息。这些技术可以让我们减少大量的内存使用，而CPU时间开销很小。我们正在计划改进程序的人机界面，并将其作为工具发布。少

Asynchronous circuits are usually modeled with a speed independent model, where the gate delays are unbounded or bounded by an unknown constant. Most of the research on design. synthesis. and verification of asynchronous circuits has been done under this model. Although the speed independent model is quite simple. the possibility of unbounded delay sometimes forces the designer to add additional complexity to the circuit.. Recently. in order to design fast, compact asynchronous circuits, the bounded delay model is often assumed. However. these timed asynchronous circuits can no longer be verified accurately using the untimed verification algorithms. Therefore. in this research, we aim at building a timed model which can properly express those timed circuits. and developing the verification algorithm based on the model, In the first year, we theoretically formalized the verification method based on timed trace theory, and proved the correctness of the implementation of the verification … More method using time Petri nets. Then, we tried to apply the partial order reduction technique, which traverses only some subset of successor states as long as the correctness is not affected, to the timed verification method. According to the experimental results obtained by a prototype, the effectiveness of the method was shown. In the second year. for the theoretical part, we proposed several definitions for the correctness based on the timed trace theory, and derived the sufficient conditions that the algorithm to check the correctness is implementable. Further. we proved the correctness of the partial order reduction algorithm that we proposed last year. For the practical part. we implemented the second version of the verification algorithm based on the partial order reduction. By using it, we could verify various timed asynchronous circuits much more efficiently than by using previous method. Further, in order to reduce the memory use in the verification method, we proposed techniques for sharing. compressing. and thinning out the visited state information. These techniques could allow us to reduce the large amount of memory use with a little overhead in the CPU times. We are planning to improve the man-machine interface of the program, and to release it as a tool. Less