Verification of desynchronized circuits

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.