Automatic synthesis and verification of hazard-free control circuits from asynchronous finite state machine specifications

The author describes algorithms and techniques underlying a CAD system for automatic synthesis and verification of control circuits based on asynchronous finite state machine (AFSM) specifications. AFSM specifications are transformed into signal transition graphs, and then into state graphs. Techniques for hazard-free synthesis techniques from state graphs are described. An efficient two-level hierarchical technique based on state graph contraction and D. Dill´s verifier (ACM Distinguished Dissertation Series) is used to verify the logic implementations against the state graph. A CAD prototype called CLASS, (Cirrus Logic Asynchronous Synthesis System) has been used to successfully synthesize and verify the HP Labs benchmark and various other real applications