Experiences with representations and verification for asynchronous circuits

As asynchronous circuits approaches overcome many critical issues such as clock skew, jitter, noise, and power consumption of synchronous technology, they are used more widely in electronic system. Their correctness should be considered carefully. The two most important issues are system representations, which are very complex due to its asynchronous behavior, and verification methods. While the combination of Petri nets and Data Flow Graph (PN-DFG) is very efficient in representing such systems, the study on verification for PN-DFG just has begun recently, including our previous works on verifying PN-DFG using NuSMV tool. In this paper we develop more this approach and extend it to many cases. Interestingly, the case studies will be provided as a benchmark set that can be used to test verification algorithms for asynchronous circuits.