Research on formal verification of asynchronous logic circuits with bounded delays

有界时延异步逻辑电路形式化验证研究

• 批准号: 09680329
• 负责人: YONEDA Tomohiro
• 金额: $ 1.54万
• 依托单位: TOKYO INSTITUTE OF TECHNOLOGY
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 1997
• 资助国家: 日本
• 起止时间: 1997 至 1998
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-09680329/
• 关键词: Formal verification; Asynchronous circuits; Bounded delay model; Time Petri nets; Timed trace theory; Partial order reduction; Partial order reduction

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

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

项目成果

Tomohiro Yoneda: "Hiroshi Ryu, Timed trace theoretic verification using partial order reduction" Proceedings of ASYNC'99. (to appear). (1999)

Tomohiro Yoneda：“Hiroshi Ryu，使用偏序约简的定时迹理论验证”ASYNC99 论文集。