A unified signal transition graph model for asynchronous control circuit synthesis

Both low-level (analysis-oriented) and high-level (specification-oriented) models for asynchronous circuits and the environment where they operate, together with strong equivalence results between the properties at the low levels, are described. One interesting side result is the precise characterization of classical static and dynamic hazards in terms of the model. Consequently the designer can check the specification and directly decide if the behavior of any implementation will depend, e.g., on the delays of the signals described by such specification.<>