Synthesis and verification of asynchronous circuits from graphical specifications
Cho W. Moon · 1992
Despite the increasingly important role that asynchronous circuits are playing in digital designs, there has been no good design methodology which can help designers deal with the difficult task of designing and verifying asynchronous circuits. Asynchronous circuits are difficult to specify, let alone synthesize, because behaviors such as concurrency, sequencing, conflict, timing constraints and data-dependency are difficult to specify in a way both natural for designers and easy for formal analysis and verification tools. Synthesis is complicated by the presence of hazards, which force designers to consider not only the static behavior but also the dynamic behavior. In addition, the absence of the controlled storage elements and the variations in delays make the verification a formidable task. This thesis deals with a design methodology which is formal, yet natural for designers, and lends itself nicely to automatic synthesis and verification. This methodology is based on a subset of a Petri-net called the signal transition graph (STG). From an STG a two-level implementation can be produced which is hazard-free under all possible gate delay variations, assuming that gates have arbitrary delays but wires have no delays and that the environment is well-behaved. The functional correctness and the hazard-free property of the implementation can be proven formally by using the finite-state models, with which behavior containment check can be performed. Unbounded gate delay provides a nice abstraction for this verification, and gives robustness to delay variations. Also, a relationship between STG and FSM is established, and from this relationship a new method to solve the state assignment problem arising from STG specification has been developed.