Verification of desynchronized circuits
Sudarshan K. Srinivasan, Raj S. Katti · 2009
Desynchronization is a method used to synthesize circuits with a high degree of asynchronicity from synchronous parents. It is well known that asynchronous circuits are hard to design and verify. We propose a refinement-based formal method to check that desynchronized pipelines correctly implement their high-level non-pipelined specifications. The method is based on an algorithm to construct functions that relate desynchronized states with specification states. The method is used successfully to check partial safety of a desynchronized implementation of the DLX architecture.