Practical hardware engineers often complain about timing problems in asynchronous circuits and state that much care should be taken before the final circuit is certified as correct. They prefer clocked products and are extremely reluctant to design asynchronous circuits because their specification and analysis require sophisticated techniques.
On the other hand, scientists working on logic design and switching theory keep trying to convince such engineers that asynchronism is both necessary in many applications and an important issue for good design. Sometimes they do so not only for practical reasons, of which they may have limited knowledge, but for purely academic purposes: asynchronous circuits, thanks to their implicit notion of time, will always provide many opportunities to create new theoretical models of their behavior, so questions about their formal treatment will arise again with each technological advance.
For the past three decades this apparently permanent controversy has been the main force behind work on how to analyze asynchronous circuits. This work has produced several formal models that describe the behavior of various types of networks, including the feedback-delay (FBD) model, the gate-delay (GD) model, the gate-wire-delay (GWD) model, and the switch-level (SL) model. These models are essentially based on forms of simulation semantics, especially the binary general multiple winner (GMW) semantics and the ternary simulation (TS) semantics. The key analysis problems these models tackle focus on checking the presence of critical races and static output hazards.
This paper’s major goal is to unite all the existing models in a unified race analysis framework called the extended multiple winner (XMW) model. This model incorporates the multiple winner aspect of the GMW concept (the delays are arbitrary and any non-empty subset of the set of unstable gates is allowed to change) and the third ×-value (the unknown or intermediate value) of the TS semantics.
The authors abstract the properties of both gate and MOS circuits and represent each circuit as a mathematical asynchronous network that consists of a directed graph with an associated set of (ternary) vertex excitation functions. They formulate network reduction rules that may sometimes help the designer to speed up the computationally costly procedures on the reduced set of vertices; in the minimum case this set is the feedback, or self-dependent, vertex set. They then concisely and gracefully prove two important theorems, which state that the results of the XMW analysis of an asynchronous network for the GD, FBD, GWD, and SL models are equivalent to those of the ternary simulation of the network. These theorems are valuable because they justify using the polynomially complex TS algorithms within the domain of nontransient behavior and static output hazards instead of working with the complete XMW state space of O(3m), where m is the number of vertices.
Brzozowski and Seger conclude that although their work settles many previously non-fit problems, further steps are desirable, especially to remedy a serious difficulty of both the XMW model and its TS accelerator--the model has an overly pessimistic state transition relation, according to which the prehistory of any race state is completely ignored and all unstable vertices have the same chance of winning a race, regardless of when they entered it. More optimistic models, such as the “almost-equal-delay” model and the models based on various restricted delay ratios between racing gates (such as Mishra and Clarke’s 3/2 rule [1]), would be more realistic for most practical design applications. Furthermore, due to the XMW model’s rejection of certain state outcomes, this analysis process would be more efficient. With the help of such models one can tackle some more sophisticated tasks of checking and verifying circuits within the same general framework. Note that the paper neglects several works on formal verification of asynchronous circuits, such as those that use temporal logic for that purpose [1]; the combination of temporal logic with the proposed framework could result in an extremely versatile analysis environment.
I would also recommend some additional reading on the topic [2]; this work is based on the analysis of semimodularity conditions for asynchronous circuits, which were originally introduced by D. Muller. Unfortunately, checking that a circuit is semimodular (has no conflict states from which an unstable vertex may become stable without changing its value) cannot be reduced to using the polynomially hard ternary simulation because semimodularity is a more general property and reportedly contains a sufficient condition for the circuit to be free from both static and dynamic hazards. Its generality also allows its use in race analysis of circuits with no input vertices (“autonomous” circuits) [3]; the paper neither discusses this case nor disallows it by the definition of a network. Such circuits are specific since they experience the cyclic operation, which cannot be regarded as a nontransient case. This operation does not, however, satisfy the definition of a transient cycle either (this seems to be the only “non-fitness” of the proposed model). On the other hand, this controversy is lessened in the XMW model because its basic assumption is that the inputs remain fixed after each change until the network has a chance to stabilize. This assumption does not fit very well in the analysis of a circuit that needs to operate in a pipeline mode whose fundamental discipline involves changing the inputs even before some of the outputs are idle.
The text and illustrations are generally good, but Figure 14 contains some confusing discrepancies between the CMOS circuit (a) and the S-graph (b) that prevent the two from “corresponding.” My overall impression of this important paper is quite positive. It will attract attention from both professional engineers and classroom scholars who have a commitment to logic circuits and modern VLSI design aids.
