Hierarchical gate-level verification of speed-independent circuits

Hierarchical Gate-Level Verification of Speed-Independent Circuits of as Oriol Roig, Jordi Cortadella and Enric Pastor * Department of Computer Architecture Universitat Politkcnica de Catalunya Gran Capit& s/n, Mbdul D6, 08071-Barcelona, Spain Abstract This paper presents a method for the verification speed-independent circuits. The main contribution the reduction of the circuit to a set: of complex gates that makes the verification time complexity depend only on the number of state signals (C elements, RS fiip-jlops) of the circuit. Despite the reduction to complex gates, verijication is kept exact. The specification of the environment only requires to describe the transitions of the input/output signals of the circuit and is allowed to express choice and non-determinism. Experimental results obtained from circuits with more than 500 gates show that the computational cost can be drastically reduced when using hierarchical verification. 1 Introduction Asynchronous circuits can be considered as a practical alternative to face some of the critical problems that appear when designing complex, low power, high performance digital systems. The clock signal in synchronous circuits enables to introduce a level of abstraction in the time domain and overlook most temporal relations among the signals of the circuit. Only the concept of critical path is relevant for the performance of the system but not for its functional correctness. Unfortunately for the designer, the absence of a clock in asynchronous circuits makes their design an error-prone task. Most difficulties come from the need to ensure that all signals are free of undesirable transitions, hazards, that can produce circuit malfunctions. The additional complexity introduced by the analysis of the temporal relations makes verification essential for asynchronous circuits. But while only the outputs of memory elements, e.g. flip-flops, are required to represent the state of a synchronous circuit, the output of all nodes (gates and memory elements) must be probed to define the state of an asynchronous circuit. Given that, in the worst case, the size of the state space can be 0(2.), TI being the number of signals to define the state, this space can become extremely large even for moderate size asynchronous circuits. Several authors have proposed verification techniques to avoid the explicit enumeration of all the *Work supported by ACID-WG (Esprit 7225), CYCIT TIC 94-0531-E and Department d’Ensenyaxnent de la Generalitat de Catalunya. states: unfoldings [ll], partial orders [14], symbolic model checking [4] and trace theory [6] among others. This paper presents sufficient conditions to automatically reduce the complexity of the circuit to be verified for speed-independence. The proposed method aims at the reduction of the number of variables required for verification. It has been combined with symbolic model checking techniques to efficiently represent the state space of the circuit. 1.1 Contributions The method presented in this paper aims at the verification of gate-level speed-independent circuits. Beerel et al. [a] observed that, if the verifier were told by some oracle that the circuit is hazard-free, checking its correctness against its specification coiild he reduced, roughly speaking, to perform a verification B la synchronous with only the outputs of the memory elements (e.g. C-elements or RS flip-flops) as state variables. Based on this observation, our approach verifies correctness in two steps: (1) satisfiability of the specification assuming the absence of hazards and (2) hazard detection. The major contributions of this paper are the following: The circuit, a flat netlist of gates, is automatically reduced to a set of complex gates. The time complexity of verification is made dependent on the number of memory elements rather than on the number of signals of the circuit. Even with the reduction to complex gates, verification is kept exact, i.e. neither false positive nor false negative verification results are possible. The environment is described by a state graph that only needs to contain the transitions of the input/output signals of the circuit. Choice and non-determinism of the environment are allowed. The paper is organized as follows. Section 2 discusses the basic ideas of hierarchical gate-level verification by means of an example. Section 3 presents some basic definitions used along the paper. Section 4 analyzes the conditions under which exact hierarchical verification can be performed. Section 5 discusses the most significant implementation issues of our verifier. Comparative results between flat and hierarchical verification are presented in Section 6. Finally, Section 7 concludes the paper. 0-8186-7098-3/95 $04.00 0 1995 IEEE 128 I I d+f cc (b) Figure 1: (a) Circuit with a hazard-free behavior, (b) The same circuit with a hazardous behavior, (c) Equivalent hazard-free complex-gate circuit. 2 Hiewrchical verification: overview This section presents hierarchical verification by means of two examples. In this section, speedindependence will be considered equivalent to hazardfreeness under the unbounded gate delay model. More precise definitions will be given in Section 3. Speed-independence is not a property of a circuit by itself but of the behavior of a circuit under a certain environment. In our framework, the behavior of the environment will be represented by a Signal Transition Graph [5] in which the output signals will be inputs of the circuit and vice versa. Figures l.(a) and l.(b) depict a circuit excited by two different environments. The circuit is hazard-free with environment (a), but hazardous with environment (b). In the latter case, a static hazard can be produced on signal d when, in the state (abcde) = (11110), the event e-- arrives before e has switched to 1. However, note that an equivalent complex-gate implementation of the same circuit (Figure l.(c)) can be hazard-free. Figure 2 shows the state graph obtained by a reachability analysis of the system in Figure l.(a). In the worst case, tthe number of states can be as lar,ge as 2” , n being the number of signals of the circuit. Verification through reachability analysis [4] would simply check that each transition produced at the outputs of the circuit can be accepted by the environment, i.e. a transition with the same label is enabled in the STG. 2.1 Functional and behavioral correct ness Two important concepts must now be introduced to set up the basis of verification: functional correctness and behavioral correctness. A circuit is said to be functionally correct if an appropriate combination of the delays of its components can produce the behavior expected by the environ-- ment . A functionally correct circuit is said to be behaw iorally correct if it produces the behavior expected by the environrnent regardless the delay assigned to each component, provided that the delays are within the margins assumed for the delay model and the technology. For speed-independent circuits, delays are in the range (0, a). (abcde) 00000 1 1000 11001 11011 11111 Fk C+ , /01000~ 1 00010 I dbeC- \eb-f ~01010] I 00011 I 01110 01111 Figure 2: State Graph of the circuit in Figure l.(a). We can say now that the circuit in Figure l.(b) is functionally correct, since by assigning the AND gate a delay shorter than the delay between the transitions b+ --+ e-, the generated behavior is the one expected by the environment. However, this circuit is behaviorally incorrect, since long delays on the AND gate may produce a static hazard on d. The circuit in Figure l.(c) is both functionally and behaviorally correct (the complex-gate architecture basically assumes zero delay for the AND gate). 2.2 Verification of functional correctness A speed-independent circuit must behave correctly for any finite delay of its components. A particular case consists in “moving” the delay of a gate to its fan-out gates. Let us take as example the circuit in Figure l.(b). We can move the delay of gate e to its fan-out gate d, and we obtain the complex gate in Figure l.(c). We refer to this kind of gate clustering as collapsing. Since all the delays are in the range (0, a), the sum of the delays of d and e is still in the same range. The behavior of the output of a complex gate is included in the behavior of the original circuit (prior to collapsing). In our framework, functional correctness is verified 129 (abed) “hazard” (b) Figure 3: (a) State graph after verification of functional correctness. (b) State graph after verification of behavioral correctness. by collapsing some of the gates of the circuit. In this way, multiple gates can be collapsed into one complex gate and, thus, internal signals eliminated for the verification. Only for memory elements (e.g. C elements) or outputs of complex gates, the signals cannot be eliminated. Verification of functional correctness becomes simpler and faster because of the elimination of internal signals. Moreover, design errors that do not depend on the delays of the gates can be detected soon, without requiring an exhaustive verification of the temporal relations among all signals. In the example of Figure l.(b), functional correctness is verified by first collapsing the AND and OR gates into one complex gate and eliminating signal e. Next, the state graph of the circuit/environment is built and verified for correctness (Figure 3.(a)). 2.3 Verification of behavioral correctness In general, large circuits will be collapsed into several complex gates. As illustrated in Figure 4, this can be done hierarchically according to efficiency criteria for verification. Figure 4: (a) Flat circuit (8 gates). (b) Hierarchical complex-gate organization (3 complex gates). The second step of verification is devoted to detect hazards inside the complex gates. Intuitively, this is performed as follows. Given a complex gate, the state graph of the collapsed circuit is projected onto the input/output signals of the complex gate. This projection maps all states with the same values for the input/output signals of the complex gate (even if they are semantically different) onto the same state. We will show that this apparent loss of environmental information is not relevant for the verification of hazard-freeness. Finally, the complex gate is verified to be hazard-free under the projected graph as environment. Isomorphic groups of gates can be mapped onto the same complex gate. In the example in Figure 4 there is a pattern repeated twice: an OR gate which inputs are an AND gate and a primary input. We will show in Section 4 that we can project the environment of several complex gates onto one single state graph and verify they hazard-freeness at a time. This hierarchy allows us to verify isomorphic subcircuits together. It is important to notice that the environment of each complex gate is calculated as if it were hazardfree. In Section 4 we will show that, even with this restricted environment, hazard-freeness can be exaclly verified. Figure 3.(a) shows the state graph of the collapsed circuit. By chance, this graph coincides with its projection onto the signals {a, b,c,d} as the whole circuit has been collapsed into one complex gate. When generating the state graph of the complex gate (Figure 3.(b)), an unexpected transition (d-) is detected in state ii010, since the corresponding state of the environment (1101) can only accept transition a-. In case the complex gate were verified to be hazardfree, its corresponding state graph would be projected onto the input/output signals of its components and the same operation would be performed at the next level of the hierarchy. This is illustrated in Figure 5 that depicts the environment of the AND gate after projecting the graph of Figure 3.(b) onto the signals (%b, ell. ‘This environment is only depicted as an example, since there is not need to derive it for simple gates or for gates contained in hazardous complex gates. 130 Figure 5: Environment of the AND gate after the projection of the state graph onto the signals a, b and e. Only one question remains to be answered: why is hierarchical verification exact? In our framework, the absence of hazards is proved by verifying that the circuit is semz-modular, i.e. no gate can be disabled by changing the value of its inputs. Let us assume that C is a circuit amd 6 is an equivalent circuit in which some gates have lbeen collapsed into complex gates and the corresponding internal signals eliminated. In Section 4 we will prove that: a) if 6 is not semi-modular, then C is not semib) if C is semi-modular but C is not semi-modular, there is a complex gate of e for which the behavior of the corresponding decomposed gate, under the prc)jection of the state graph of 6 onto the input/outputs of the gate, is not semi-modular. Conjecture a) guarantees no false negatzves, Why is hierarchical verification more efficient ? A critical factor that determines the complexity of verification is the number of signals of the circuit. With hierarchical verification the number of signals relevant at each step of the verification is drastically reduced: during verification of functional correctness only the input/output signals of the complex gates are required; during verification of behavioral correctness of a complex gate only the interface and internal signals of the gate are required. There is only one limit to the minimum number of variables required for functional verification: the number of output signals of the memory elements, such as C-elements or RS flip-flops. modular either. h whereas conjecture b) guarantees no false posztzves. 2.4 approach impractical when a flat netlist of gates, with no explicit hierarchical organization, must be verified. Following Dill’s approach, a subset of gates of the flat circuit (potentially substitutable by a complex gate) should be substituted by an equivalent trace structure. Not knowing how the environment of the complex gate will be inside the circuit, the trace structure should consider all possible input/output transitions and, therefore, include the state of all internal signals, which would preclude the subset of gates to be handled as a complex gate. Conservative verification Beerel et al. [2] also propose a two-step approach. After verifying the circuit is complex-gate equivalent to its specification, hazard-freeness is verified by subsequently checking the monotonicity and acknowledgment of all signal transitions. A cube approximation that overestimates the set of states of the circuit is proposed to conservatively prove the absence of hazards. Although never found in the examples presented by the authors, false negatives are theoretically possible. Other limitations of this approach are that it is limited to externally-cut circuits (all memory elements must appear in the specification) and that the specification of the circuit is not allowed to express output choice (arbitration). Polynomial methods for signal graphs Kishinevsky et al. [7] presented a polynomial algorithm to verify distributivity (a subclass of speedindependence) from circuit behaviors described by signal graphs. The main limitation of their approach is that the signal graph must specify the transitions of all signals of the circuit and that neither choice nor non-determinism are allowed in the signal graphs. 3 Definitions We will consider a circuit to be a set of gates connected to an environment. The behavior of the environment will be modeled by means of a state graph. In our verifier, the state graph is derived from a Signal Transition Graph that describes the interaction of the environment with the input/output signals of the circuit. Thus. environments with choice and non2.5 Related work determinism are allowed. In this section, some of the most relevant efforts related with t8he verification of speed-independence and closest to the approach described in this paper are presented. Hierarchical verification Definition 3.1 (Circuit) A circuit is a pair C = (A, “1, where A = {al, ..., a,} is a set of signals (. = AI) and F maps each signal a; E A to a boolean function f; of arity n, that represents the function compuied by the gate that drives a;. In his thesis [B], Dill already proposed hierarc!hical verification of speed-independence: if a component conforms to a trace structure, the behavior of that component can be safely substituted by the trace structure. However, this approach requires the designer to identify the basic components of the circuit and know their expected behavior in advance. This makes the Definition 3.2 (Fan-in and fan-out of a signal) The fan-in of signal a; E A, fanin(a;) C A, is ihe set of signals that fi depends on. For gates that hold state, a; E fanin(a;). The fan-out of signal a; E A, fanout(a;) C_ A, is the set of signals that depend on ai, i.e. fanout(a;) = {ak E Ala; E fanin(ak)}. 131 Definition 3.3 (State graph) A state graph (SG) is a 4-tuple, (A,S, E,X), where A = {a1 ,..., a,} is the set of signals, S is the set of states, E C S x S is the set of transitions and X is the labeling function for states that maps each state with a bit-vector over A. The fact that (s, s’) E E will be also denoted by SES’. E* denotes the transitive closure of E, and sE*s‘ denotes that there is a path from state s to state s’ in the state graph. In those cases jn which the labeling function is the identity, the state graph will be denoted simply as (A, S, E). Definition 3.4 State graph of a circuit The state graph of a circuit C = (A, F) with initial state so is a state graph, SG(C, so) = (A, S, E), such that S and E are strictly defined by the following recursion: 1. so E s . 2. [(S E S)A(Vi#kSi = Si)A(SL # Sk)A(SL = fk(s))] ==+ [(s’ E S) A (s, s‘) E E] . Relation E can be partitioned into n subsets as follows: Ei = {(s,s’) E Elsi =Si} , E = UEi. a,EA Note that the labeling function X is the identity. This means that each state s E S is a bit-vector over A such that the ith element of s, denoted by si, specifies the value of signal ai in state s. Given a state s E S, if there exists s’ E S such that sEis‘ we will say that signal ai is excited in state s. Otherwise we will say that ai is stable in s. Definition 3.5 (Projection of the state graph of a circuit) Given the state graph of a circuit, SG(C, so) = (A, S, E), and a subset of signals X C A, the projection of SG(C,so) onto X is a state graph, Vs = (SI ,... , Sn) E s, projx(s),= (SI,..., Sk), i.e. the sub-vector of s containing only the signals in X (we assume 1x1 = k and X to be the first IC elements of A), projx(S) = (~’13s E S : projx(s) = s’} , P..& (E) { (Pro& (s) 9 Pro& ( 4) I SE’ s’ and only one signal in X transitions from s to s’} . = Note that the definition of a state as a bitvector implies that semantically different states can be projected onto the same state (i.e. projx(s) = projx (s’) = i’ and s # s’). The following proposition is a result of the previous definition. Proposition 3.1 Let C = (A, F) be a circuit, SG(C, so) = (A, S, E) its state graph, and fanin(ai) U {ai} & X E, A. Let projx(SG(C,so)) = (X,s^,@ be the projection of SG(C,so) onto X. Let s,s’ E S and SE S such that projx(s) = projx(s’) = 2. Then ai excited in s e ai excited in s’ e ai excited in i? . Proposition 3.1 is crucial for our method, since it states that the excitation/stability of a complex gate (and subsequently semi-modularity) can be locally checked by only knowing the values of the input/output signals of the gate and regardless the state of the rest of the circuit. Without loss of generality and for the sake of simplicity, we will consider autonomous circuits, i.e. with no interface, for verification. The obtained results can be naturally extended to circuits with interface. Next, observational equivalence [12] is defined. This is a concept that establishes an equivalence among those circuits that produce the same events on a given set of signals. For simplicity, we will use a restricted definition, since we are only interested in circuits in which the signals of one of them is a subset of the signals of the other. Definition 3.6 (Observational equivalence between two circuits) Let C = (A, F) and 6 = (X, @) be two circuits with X C A, and let SG(C,so) = (A,S,E) and SG(G,?’) = (X,,!?,,f?) be their state graphs. C and C are observationally equivalent from so and ?’ respectively iff: h h I. if’ = projx(so) . 2. Vs E S,? E s^ such that 2 = projx(s) and Vai E a) if sEis’ then 31 E s^ such that Z&? and b) if ?,!$? then 3s‘ E S such that sE>EjE>s‘ where E: denotes any sequence of non-observable transitions. X: 9s - p.ojx(s’) . and Z’ = projx(s‘) . In this paper we propose to verify semi-modularity rather than speed-independence. Semi-modularity is more robust than speed-independence and both concepts are tightly related for most practical cases, as subsequently explained (see [17] for further details). Definition 3.7 (Semi-modularity) A signal ai is semi-modular with respect to signal ab E fanin(ai) (ai # ak) if the gate that drives ai, having been excited, cannot become stable by changing the value of ak. In terms of the SG of the circuit, a signal ai is semimodular with respect to ab in SG(C, so) = (A, s, E) iff sE~s’ * [si # fi(s) ==+ # fi(~’)] . 132 f4 = a3 . a5 + a4 . (a3 + as) f4 := a3 . (a1 + a2) + a4 . (a1 + a2 + u3) Figure 6: O:R and C gates collapsed into a complex gate. A signal ai is semi-modular if it is semi-modular with respect to ar‘l its fan-in signals. A circuit is semimodular if ail its signals are semi-modular. Definition i3.8 (Strongly-live circuit [17]) A circuit is strongly live zff its state graph is strongly connected and for each signal ai there exists a state s E S in which ai is excited. Theorem 3.1 ([17]) If a circuit is strongly live, then the circuit is speed-independent iff it is semi-modular. 4 Reduction to complex gates This section provides the means that enable to elim-. inate some signals of a circuit to simplify its verification. We propose to collapse several gates into one complex gate with the same functional behavior and eliminate the internal signals. Let us assume we have a circuit C = (A,F) with signal a, being driven by a combinational gate, Le. a, @ fanin(a,). Let us build a new circuit e = (X, F), with X = A-{a,}. Let 2= projx(s) and the boolean expressions of the gates of e defined as follovvs: h if a, 4 fanin(ai) , ifa, Efanin(ai) . Note that the above expression substitutes s, by f,(s) and, therefore, fi(2) does not depend on s,, as a, fanin(a,). Figure 6 shows how the boolean expression of a complex gate is derived from the expressions of the simple gates. In case ]fanout(a,)l > 1, multiple complex gates will be created, as illustrated in Figure 7. h Theorem 4.1 Given two circuits C = (A, F) and e = (X,P), with X = A - {a,} and dejined as above, and their state graphs, SG(C, so) =AA, SI E) and SG(e, projx(so)) = (X, 2, g). C and C are observationally equivalent from so and proj, (so) respectively iff all signals in fanout(a,) are semi,-modular with respect to a, in SG(C,sn). Proof Condition 1 of definition 3.6 holds by construction. Let s E S, 2 E S, g = projx(s) and ai E X. In those cases where we prove that fa(s) = f;(Z), it immediately follows that obsezvational equivalence holds. More precisely, fi(s) = fi(g) = si implies that ai is stable in both s and S and, therefore, conditions 2.a and 2.b hold. If fi(s) = fi(2) = Si there exist s’ and s such that sEis’ and SEi? and ? = projx(s’), since the same signal transitions from s and 2. Therefore, conditions 2.a and 2.b also hold. If a, @ fanin(ai) then s(2) = fi(s) and, therefore, observational equivalence holds. If a, E fanin(ai) then h h h h /y h fi (2) = fi(S1,. . . , Snl,O).K(.)+fi (s1 ,. . . , S,-l,l).fn (s). 1 semi-modularity observational equivalence I ~ ~~~ Since ai is semi-modular with respect to a,, a change on signal a, cannot disable ai. Hence, fi(s) does not depend on s, when signals ai and a, are simultaneously excited, i.e. It only remains the case which describes the situation in which ai is stable, a, is excited, and fi(s) depends on the value of signal a,. Hence, h fi(2) = K(s1,. .., Sn-l,l).S,+fi(S1,...,S,-l,l).~n - - - f;(s) = si . Clearly, condition 2.a holds for state s, since ai is not excited in s. To prove 2.b, let us take ? such that 133 Figure 7: (a) Gate with multiple-fan-out. (b) Complex gate considered for functional correctness (c) and for behavioral correctness. h 2EiS’. We will prove that there exist s’, s” E S such that sE,s“Eis‘ and S’ = projx(s’). Since a, is excited in s then we have s“ E S such that sE,s”. But now, ai is also excited in s” as - fi(S1,...,sn-1,0) = -f’i(~~,...,sn-~, 1) , and thus there exists s’ E S such that d’Eis’. Finally, s and s’ only differ in the ith and nth elements and therefore 2 = projx(s’). 17 semi-modularity -3 7 observational equivalence I If ai is not semi-modular with respect to a,, then 3s,s‘,s// E S such that sEis’, sE,s” and ai is not excited in s”. Since only a, changes between s and s“, we have that s = projx(s) = projx(s/’). Thus, h Since ai is excited in s and stable in s” (after a transition of a,) then fi(s1,..., sn-l,~) = fi(sl,..., sn-1,1) . Moreover, fn(s) = S, and fi(s) = Si, as a, and ai are excited in s. Therefore, h fi(2) = f;(sl ,..., sn-1,1) ‘sn + fi(sl,..., sn-1,1) ‘5, - = fi(S) = si , which means that ai is not excited in 2 and, therefore, condition 2.a does not hold. 0 Theorem 4.1 is the basis to prove that hierarchical verification is exact. This is the purpose of the next corollaries. Corollary 4.1 C not semi-modular from 9 ==+ C not semi-modular from so. h Proof This immediately follows from the fact that the state graph of e is the projection of the state graph of c. 0 Corollary 4.1 guarantees that hierarchical verification will not give false negatives. Corollary 4.2 If 2 is semi-modular from and C is not semi-modular from so, then either a, or some signal ai E fanout(a,) are not semi-modular in C. Proof (by contradiction) Assume that a, and all its fanout signals are semi-modular. Then, by theorem 4.1, C and e should be observationally equivalent. Since C is semi-modular and C is not semi-modular, then a, (the only non-observable signal) should be non-semi-m-odular, which contradicts the initial assumption. 0 Corollary 4.2 shows that hierarchical verification does not produce false positives. Consider a complex gate that drives ai E fanout(a,), and that Xi is the set of input/output signals of the gate, i.e. h x, = (ai} U (funqai) - {a,}) Ufunin(a,) . It can be derived that, by taking projx,(SG(e,2’)) as the environment of the complex gate, and SE as the initial value for signal a,, non-semi-modularity of ai and a, in SG(C, so) is also detected in projx, (SG(e, 2’)) (by proposition 3.1). Intuitively it can be proved by showing there is always one state s of C in which non-semi-modularity is manifested for the first time from so. Because of the observational equivalence while semi-modularity holds from so, the projection of s ontoAXi will also belong to the set of states of projx,(SG(C,?’)). 4.1 Environment of a complex gate and circuits with environment Complex gates obtained from collapsing can be seen as externally-cut circuits [l]. An important property of externally-cut circuits is that they have no hidden state. The state of such circuits is completely captured by the values of the interface signals, i.e. the values of the interface signals uniquely define the value to which all internal signals would eventually settle if the interface were held fixed [l]. This follows from the fact that memory elements in externally-cut circuits can be regarded as combinational gates when given an interface state. For example, a C-element will operate as an AND gate in those states in which the output is zero, but as an OR gate if the output is one. The projection of the state graph onto the interface signals will keep the edges involving interface signal switches (see proposition 3.1). This projection, however, may fold semantically different states onto the same state, thus introducing additional nondeterminism (choice). Nevertheless, input choice is 134 not a problem because in the second verification step we are dealing with externally-cut circuits. Since there are no hidden variables, the circuit reaction will depend only on the state and on the signal that has switched. Therefore, the behavior of an externally-cut circuit in such cases will be the same independently of whether theire is a state with nondeterministic choice or two different states (with deterministic choice). Let us assume that a circuit has several iinstances of the same l(comp1ex) gate. Figure 8 shows two AND gates of the same circuit with a different environment for each. As previously mentioned, the environment of a complex gate is calculated as the projection of the state gratph onto X,. In this is example the states labeled with 010 of the environment of G2 result from the projection of two different states2. To verify the semi-modularity of each AND gate, we calculate the union of the environments of all AND gates of the circuit (environment for the generic gate G in Figure 13). This many-to-one mapping may introduce choice and/or non-determinism not manifested in the initial state graph. In fact, the set of sequences of transitions accepted by the union of projected state graphs can be larger than the union of the sets of sequences generated by each individual gate. However, semi-modularity is a local property of a gate that needs to be checked only between adjacent states of its environment. Since any transition of the projected state graph results from at least one projection of the original state graph, verification is not pessimistic but exact. Interestingly, if the union of the projected state graphs produces a semi-modular behavior of G (the generic gate), it also describes a set of sequences of events that, if applied to each gate individually, would produce a semi-modular behavior. Needless to say that, with the previous considerations, the presented approach allows to verify circuits against an environment described by a state graph, possibly containing choice, non-determinism and/or state variables that do not correspond to values of input/output signals. 5 Impleimentation issues A verifier based on symbolic model checking has been implemented. Its inputs are a Signal Transition Graph, describing the behavior of the environment, and a netlist of gates. The environment only needs to specify transitions of the interface signals of the circuit. Input/output choice and non-determinism are allowed. The markings (states) of the Signal Transition Graph are symbolically represented by using encoding techniques such as the ones presented in [8]. Disjunctively partitioned transition relations and breadth first search algorithms for symbolic traversal [4] htwe been used to calculate the set of reachable states. Next, some implementation issues are discussed. 'For the sake of clearness, they are depicted as different states in the fiigure 5.1 Reduction to complex gates The algorithm currently implemented is very simple. Each combinational gate is collapsed with its fanout gates. Only when the output of a combinational gate is one of its inputs (feedback loop), the reduction is not possible. At the end of the reduction step, only one signal for each memory element and combinational loop is kept. These signals are the ones used for functional verification. 5.2 Output choice Circuits with output choice (arbitration) can also be verified with our method. The non-semimodularity of arbitration signals (e.g. outputs of a mutex) is considered hidden inside the gate and not manifested externally. This requires a special ad-hoc description of arbitration elements in the library of gates. For example, a mutex element with two inputs (RI,R2) and two outputs (Al,A2) can be modeled by two boolean equations: AI = RI A E; A2 = R2 A In this case, non-semi-modularity is allowed for A1 and A2 with respect to A2 and A1 respectively. 5.3 Isochronic forks Verification of speed-independence assumes that wire delays are negligible with regard to gate delays. As shown in Figure 7, gates with multiple fan-out are split into several instances, each one collapsed with one of the fan-out gates. However, forks must be considered isochronic during the detection of hazards on the internal signals. Therefore, gates that share some input signals must be simultaneously verified for behavioral correctness, with only one common instance of the multiple-fan-out internal gates. As it is shown in Figure 7.(c), signals a5 and a6 must be simultaneously verified with only one instance of the gate that drives a7. This would not be necessary if delayinsensitiveness were verified, since forks are not assumed to be isochronic. 6 Experimental results Table 1 reports the results obtained from running several experiments on our verifier. All the examples are scalable, i.e. they can be enlarged by simply increasing the number of instances of the basic cells. However, their intrinsic regularity has not been exploited to verify the circuit. The examples used are the following: master-read (obtained from automatic synthesis tools), a Distributed Mutual Exclusion (DME) circuit [9, 61, a tree arbiter [lS], an asynchronous FIFO [IO], a register file [I31 and a demultiplexer [3]. Results on flat (no reduction to complex gates) and hierarchical verification are shown3. The number of signals for hierarchical verification corresponds to the 3F~r the DME, results are comparable to those presented in [4] when multiple initial states are used. Here, we only present results obtained with one initial state (to avoid taking advantage of the regularity of the circuit) 135 cl000 - 010 al++ tbl100 011 bl+i tal110d 111 Cl+ 01 0 001 Figure 8: Union of environments for different instances of the same gate. number of states signals of the circuit, since all combinational gates are eliminated. All the circuits are dominated by memory elements. The one with most combinational gates is the DME (half of the signals). The FIFO is a peculiar case, as all the signals are outputs of memory elements and, therefore, no difference exists between flat and hierarchical verification. The reported BDD sizes are the largest ones encountered during the traversal of the circuit. The CPU time of hierarchical verification is mostly dominated by the first step (functional verification). The number of states of hierarchical verification is the one obtained during functional verification. The size of the BDDs, often crucial to avoid running out of space, is reduced by the fact that many variables are eliminated when reducing to complex gates. The significant improvements in CPU time are basically due to two factors: 1) the reduction of the size of the BDDs and 2) the reduction of the logic depth of the circuit, which directly influences on the number of iterations required to reach a fixed point during the traversal. The presented results confirm that hierarchical verification makes time complexity depend on the number of state signals of the circuit, rather than the number of gates. We believe that even better results can be obtained for circuits generated by automatic synthesis techniques, in which the ratio of combinational gates may be higher. However, at this moment there are no examples large enough to be considered critical for verification (the largest ones can be verified in roughly a dozen of seconds). As tools for synthesis and composition of circuits become mature, the complexity of the circuits will increase significantly. 7 Conclusions The complexity of formal verification of asynchronous circuits fundamentally depends on the size of the circuit, i.e. the number of gates. Reducing the size of a circuit by collapsing gates into complex gates only allows a partial verification in which a false positive might be given as result. In this paper, sufficient conditions for hierarchically verifying speed-independence have been presented. It has been shown that an exact verification can still be done if the circuit is reduced to complex gates and the environment of each complex gate is calculated during the verification of functional correctness. Circuits are allowed to be verified against an environment that may specify input/output choice and non-determinism. A verifier based on symbolic model checking has been implemented and several experiments with large circuits reported. It has been shown that, by reducing the number of relevant variables during verification, both the size of the BDDs and the computational cost drastically drop. As future work, techniques for regularity extraction will be explored [15]. They should allow to further reduce the computational cost of those circuits in which combinational gates dominate over memory elements. Acknowledgments We would like to thank Lucian0 Lavagno, Alex Yakovlev, Michael Kishinevsky and Alex Kondratyev for numerous insightful discussions on improving the clarity and presentation of this work. References [I] P. A. Beerel. CAD Tools for the Synthesis, Verification, and Testability of Robust Asynchronous Circuits. PhD thesis, Stanford Univ., Aug. 1994. [a] P.A. Beerel, J. R. Burch, andT. H.-Y. Meng. Sufficient conditions for correct gate-level speed-independent circuits. In Proc. Int. Symp. on Advanced Research in Asynchronous Circuits and Syst., pages 33-43. IEEE Computer Society Press, Nov. 1994. 131 P. A. Beerel and T. H.-Y. Meng. Semi-modularity and testability of speed-independent circuits. Integration, the VLSljournal, 13(3):301-322, Sept. 1992. 136