SYNCHRONOUS REALIZATION OF ASYNCHRONOUS COMPUTATIONS

A circuit can be described as an asynchronous computation. Such an abstract description allows formal verification and refinement. However, to realize the description as a traditional clocked circuit, a synchronous description is more appropriate. We present a sufficient condition, called an implementation condition, on an asynchronous program which allows a very simple transformation into a synchronous circuit. To check that a given program meets the implementation condition we use a mechanical theorem prover and a front end to generate the proof obligations from the asynchronous circuit description.