Synthesis of Verifiably Hazard-Free Asynchronous Control Circuits

A synthesis technique for asynchronous sequential control circuits from a high level specification, the Signal Transition Graph (STG) is described. The synthesis technique is guaranteed to generate hazard-free circuits with the unbounded gatedelay model and the bounded wire-delay model, if the STG is live, safe and has the unique state coding property. A proof that STG persistency is not necessary for hazard-free implementation is given. 1 Introduction Asynchronous sequential circuit design has always been a controversial topic. In the early years of electronic circuit design, when the size of the circuits was such that a human designer could keep track of the complex timing issues involved, it was a popular design style (see [Ung69] for a thorough review). Then synchronous logic dominated the VLSI era, when the ease of design of clocked circuits overwhelmed the advantages of the asynchronous style. Asynchronous design, still, has always been around, at least in the restricted domain ..