Research on formal verification of asynchronous logic circuits with bounded delays

点击翻译按钮获取中文摘要

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