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