Modeling and Synthesis of Timed Asynchronous Circuits
Peter Vanbekbergen Synopsys Inc. Mountain View, CA 94043-4033 Gert Goossens IMEC Laboratory B-3001 Leuven, Belgium
WRITE
0-inf
Bill Lin IMEC Laboratory B-3001 Leuven, Belgium
d
30-100
Abstract | Most asynchronous compilers do not take into account timing constraints, although these are crucial for industrial interface applications. In this paper we extend the classical signal transition graph model such that timing constraints can be modeled in a concise way. We also propose synthesis algorithms that transform the initial speci cation such that the circuit derived from the transformed speci cation satis es all timing constraints.
The classical signal transition graph model (STG-model) 3, 12] has been proven to be an attractive model for the speci cation and synthesis of asynchronous controllers. Because it is based on Petri nets 7] it is very well suited to model concurrency and conditional behavior. Several synthesis techniques starting from the STG-model have been developed 3, 4, 12, 11]. The classical STG-model is intended for controllers in selftimed systems (also called self-timed controllers). In selftimed systems all system events occur in a particular sequence, but nothing ever has to occur at a particular time. In most interface applications the controllers do not follow the self-timed principles. The ring time of the transitions is constrained. For that reason the STG-model can be extended to represent timed systems, by connecting timing information to the arcs in the STG. This timing information is used to constrain the ring time of the transitions. This timing information can be interpreted in di erent ways. These di erent interpretations are called the ring semantics . Not all arcs in a timed speci cation are \causal" arcs. There are two di erent types of relations in a speci cation, namely speci cation relations and delay relations . Delay arcs indicate how an existing circuit reacts, and specify its delay characteristics. Speci cation relations indicate the time range in which the synthesized circuit should react if synthesized correctly. These di erent interpretations given to the arcs are called relational semantics . In Figure 1(a) part of the speci cation of a RAM-interface is shown. On the input signal WRITE a pulse will be generated (by the environment) of length between 30 ns and 100 ns. In response to this pulse, another pulse should be generated on the output signal CS of length between 80 ns and 200 ns. Moreover, the signal CS should have gone high before WRITE goes down again. How is this expressed by the arcs in Figure 1? In Figure 1, \delay arcs" are labeled with a \d" and \speci cation arcs" with an \s". For example, the arc between the up- and down-transition of the signal WRITE is a delay arc. It indicates that the environment will generate a pulse of duration between 30 ns and 100 ns. A delay relation can also be used to characterize the response delay of an internally generated event. This is for
s
s
0-inf
CS (a)
s
80-200
1 Introduction
WRITE d s CS
0-inf
d
30-100 0-20
s
0-inf
d s
0-20
80-200 80-100
d
d
0-20
d
80-100
DELAY (b)
Figure 1: (a) The initial speci cation with speci cation relations (labeled with an \s") and delay relations (labeled with a \d"). (b) A transformed STG that is time-consistent. All speci cation relations are satis ed by the delay relations. The signal DELAY represents the behavior of a delay line that has been added to satisfy the speci cation relations. instance the case for the delay arc WRITE + d(0;20) CS + . ! The speci cation arc CS + ! CS ? indicates that on the output signal a pulse should be generated of length between 80 ns and 200 ns. This is a speci cation constraint in the sense that a circuit should be designed that generates a pulse within the speci ed interval. An important synthesis problem is to come up with an implementation where all speci cation relations are satis ed (Section 5). This will be done by transforming the STG. Signals and/or arcs will be added to the STG in order to satisfy all the speci cation relations. This corresponds to the following design decisions: The decision on which transition of the clock (or possibly transition of another signal) signal transitions should be triggered in order to satisfy the speci cation relations. The addition of delay-lines in order to satisfy certain speci cation relations. This means that these design decisions are treated in one consistent framework. All timing details, which are often overlooked by the designer, are taken into account. The synthesis process is basically a two step process. In the rst step arcs and/or signal transitions are added to satisfy the speci cation relations. In the second step transforma-
Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or speci c permission. (c) 1994 ACM 0-89791-687-5/94/0009 3.50
write
delay
t1
0 135? oo
cs
60
50?80
t2
0? oo t3 0?20 150
Figure 2: Circuit implementation of the STG presented in Figure 1. tions are performed to make the circuit race-free Now, hazardelimination techniques may be used to derive a glitch-free circuit that satis es the constraints. In the example of Figure 1 we concentrate on the rst step. A possible STG that corresponds to an implementation of the STG of Figure 1(a) is + shown in Figure 1(b). The delay arcs WRITE + ! CS , DELAY + ! CS ? and WRITE ? ! CS ? all represent the delay behavior of the logic implementing the STG. These delay arcs actually "implement" the speci cation relations. The speci cation relation WRITE + +! CS + is implemented by the +delay arc WRITE + ! CS . The speci cation relation CS ! CS ? is satis ed in a more complex way. First a delay-line is added to the STG. Its behavior is represented by the signal DELAY in the STG of Figure 1(b). Then the appropriate delay arcs were added that represent the behavior of the logic. In this case the speci cation relation CS + ! CS ? is satis ed by the delay arcs CS + ! DELAY + and DELAY + ! CS ? . The implementation of the time-consistent STG is shown in Figure 2. The organization of this paper is as follows. In Section 4, the timed STG-model is introduced in a formal way. In this section the ring semantics and relational semantics will be explained. In Section 5, the basic synthesis problems due to the introduction of timing constraints are explained, and solutions are proposed. A technique is proposed to transform a time-inconsistent STG into a time-consistent STG. The relation between the timed STG and the transformations to eliminate state assignment problems will be brie y discussed. In Section 6 a synthesis example is discussed.
50?80
30?40
160
t4
t5
185
Figure 3: An STG with time intervals connected to the arcs in order to constrain the ring times of the transitions. Next to the transitions a number is indicated corresponding to a ring time that satis es the constraints ( ring time assignment).
2 Previous Work
The synthesis methods proposed by Myers and Burns are aimed at self-timed circuits but take into account timing to optimize or to size logic 6, 2]. Myers 6] proposes an event-rule based system for the synthesis of timed asynchronous circuits. This work only treats the problem of transforming the initial speci cation to satisfy the timing constraints in a restrictive way. It does not add delay-lines and does not change the edges on which signals are triggered. Rokicki 8] has proposed a timed Petri net model with relational semantics for general Petri nets. This work concentrates on an e cient method to nd the states that are unreachable due to timing constraints and a way to check whether the Petri net is time-consistent. It does not treat the problem of transforming the speci cation to satisfy all timing constraints. Borriello proposes an asynchronous compiler that takes into account timing constraints during the synthesis process 1]. The transformations proposed in 1] are based on ad-hoc rules, which are di cult to verify formally. The major advantage of event graphs in comparison with our approach is that it can handle "synchronous" timing constraints (based on the number of clock cycles). Currently, this is not considered in
The STG-model 3] is commonly used to specify the behavior of asynchronous control circuits. A Signal Transition Graph (STG) is an interpreted Petri net, hT; P; F;m0 i. T is a set of transitions, s+ denotes the up-transition of the signal s, s? denotes the down-transition of the signal s. P is a set of places which can be used to specify con ict or choice. F represents the ow relation between transitions and places; namely, F (T P ) (P T ). A marking is a non-negative integer labeling of the places m : P 7! Z+ , denoting the number of tokens in a place p. s also denotes any transition of the signal s. A marked graph (MG) is a Petri net 7] where each place p has exactly one fanin and one fanout transition. It will be represented by graph G, where the vertices correspond to transitions and the arcs to places. Given a marking m, a transition is enabled and may be red from this marking if all its fanin places have at least one token in m. An STG with no state assignment problem is said to satisfy the CSC-requirement 3, 9]. In this section timed signal transition graphs will be formally introduced. In Subsection 4.1 the ring semantics will be brie y introduced. In Subsection 4.2 the relational semantics will be presented. Based on these de nitions the notions of a time-consistent and time-inconsistent STG will be explained. In this paper only acyclic marked graphs are considered.
3 Classical Signal Transition Graphs
the approach presented in this paper.
4 Timed Signal Transition Graphs
4.1 Firing semantics
In this section we will give a very brief introduction on the ring time assignment. For a more elaborate discussion the reader is referred to 9]. The numbers indicated next to the transitions in the net of Figure 3 correspond to a speci c execution of the net. Each number indicates the time at which the transition res (occurs) for that speci c execution of the net The assignment of ring times to transitions is represented by the function # : T ! R+ . The min-max interval connected to each arc in this gure is used to constrain the ring times of the transitions. minf (p) corresponds to the minimum value assigned to arc p while maxf (p) corresponds to the max-value assigned to arc
p. The are di erent ways in which the min- and max-values
max (minf (p) + #(s(p))) #(t) p2 t\P #(t) p2 t\P (maxf (p) + #(s(p))) max
0 0
can constrain the ring times 9]. In this paper we will use the following equations:
User estimation causal arcs
input-delay relations Initial STG Consists of specification relations delay relations Make STG time consistent ADD specification relations output-delay relations ADD specification relations
(1)
CSC satisfaction
It is clear that there usually is more than one valid ring time assignment. In the sequel it is necessary to take into account all possible ring time assignments. So the complete set of ring time assignments that satisfy the constraints imposed by the places in the set P 0 is represented by ( S ; P 0 ). Note that we are considering a subset P 0 of the set of all places P . P 0 will be associated with the delay places or with the speci cation places in the next section. A timed STG is obtained by assigning a min-max timing interval to each place and by partitioning the set of places P in a set of places corresponding to the delay relations (Pd )and a set of places corresponding to the speci cation relations (Ps). An STG is called time-consistent if all its speci cation relations are automatically satis ed, when only the delay relations are taken into account. In other words, all possible executions of the net that are imposed by the delay relations should automatically satisfy the constraints imposed by the speci cation relations. An STG S is time-consistent i ( S ; Pd ) ( S ; Ps ) So the set of all ring time assignments, which are valid for the delay relations, should be a subset of the set of all ring time assignments, which are valid for the speci cation relations. In the algorithms of Section 5.2 a function will be used. This function has the following meaning. Let p be a place corresponding to a speci cation relation between two transitions t1 and t2 . minf (p) and maxf (p) are assigned to place p. The minimum and maximum time distance between t1 and t2 based only on the delay relations should reside in the interval indicated by minf (p) and maxf (p). This is denoted by ( S ; p) = 1. (An algorithm that performs this timing analysis is presented in 5, 9].)
t refers to the set of all input places of t. s(p) refers to the (unique) input transition of place p.
Derivation of next state functions
Optimization and hazard elimination
Technology mapping
4.2 Relational semantics
Timing analysis
Figure 4: Survey of the synthesis process taking into account timing. During synthesis the controller decides where and how to add new circuitry. This is performed at STG level by adding delay and speci cation relations and possibly by adding new signals with new transitions. This synthesis process consists of two steps (see Figure 4). In the rst step relations are added to make the STG time-consistent. In the second step relations are added to make the STG satisfy the CSC requirement 9]. This section is organized as follows. The speci c reasons why the three types of relations are added to the STG, are discussed in Subsection 5.1. In Subsection 5.2 an algorithm that transforms a time-inconsistent STG into a time-consistent STG is derived. In Subsection 5.3 the relation between the timed STG and the transformations that satisfy the CSCrequirement are presented.
5.1 Addition of new relations to an STG
5.1.1 Adding output-delay arcs
5 Synthesis of Timed STGs
After having de ned the ring and relational semantics of a timed STG, it will be discussed how this re ects on the synthesis of a timed asynchronous controller. An overview of the synthesis process is given in Figure 4. In the initial STG speci cation only input-delay relations and speci cation relations are present. No output-delay relations are present yet. Output-delay relations are delay-relations pointing to transitions of output signals, input-delay relations are delay-relations pointing to transitions of input signals. The input-delay relations represent the (known) behavior of the signals produced by the environment. These signals are input signals for the synthesized circuit. The speci cation relations specify in which range in the time domain the controller should react.
The exact delay characteristics of the logic are only known when the logic has been generated. Unfortunately, no logic can be generated before the CSC requirement is satis ed. Output-delay relations are added to satisfy the CSC requirement. So this is a classical chicken-egg problem. To break this vicious circle the following simpli cation is proposed. The user should give an estimate of the delay of the logic, and the compiler uses this estimate during the synthesis of the STG. All the transformations on the STG are performed based on this estimate. Once the logic is technology mapped to a certain library a timing analysis tool 8] checks whether the assumptions made by the user are correct. If not, the user is forced to adapt the assumption made for the output-delay relations or he may even be forced to change the original speci cation. So there is a loop over the synthesis process. This is schematically presented in Figure 4. An example of this process is discussed in Section 6.
a+
0-20 25-inf d d 25-inf
a+
d
d 0-20 s 25-inf
a+
d 0-20 d d
a+
d 50-70
b+
s 75-inf d
u+
0-inf
b+
75-inf d
u+
0-inf s
0-inf 75-inf
b+
d
u+
s
0-20
a+
d 50-70
o+
s 0-inf
0-inf
a circuit under design b
b+ circuit
s 0-inf
b a o under design
as 0-inf
a(a)
a(b)
a(c)
Figure 5: (a) A time-consistent STG. (b) The same STG with a valid speci cation arc added. (c) The transformation that is prevented by the arc added in (b). It is assumed that all output-delay relations are always assigned a minimum value and a maximum value that is set by the user. These values will be referred to as mindelay and maxdelay . The user is discouraged to use a non-zero mindelay value. Speci cation relations may be added by the compiler. This means that the compiler is tightening the speci cation set by the original speci cation relations. Intuitively this is done to specify additional precedences that have to be satis ed. These additional precedences are useful to satisfy the CSC requirement. An example is presented in Figure 5(a). Assume that the synthesis algorithm, which transforms the STG to satisfy the CSC-requirement, requires putting u+ between a+ and b+ . So a speci cation relation has been placed between u+ and b+ (Figure 5(b)). This has to be a speci cation relation. An input-delay arc would change the behavior of the signal b, which is an input signal. It is not allowed to change the behavior of the environment. One could argue that it is not necessary to add the speci cation relation, because a simple timing analysis on the STG of Figure 5(a) shows that u+ always precedes b+ . But in the STG of+Figure 5(a) it is still allowed to add a delay relation from b to u+ which results in the STG of+ Figure 5(c). This STG is also time-consistent. In this case u does not re any more between a+ and b+ . The addition of such a delay relation is actually prevented by the addition of the speci cation relation in Figure 5(b). If the system is time-consistent after the addition of a new speci cation relation the original system before the addition of the speci cation relation is also time-consistent. So this corresponds to a valid transformation.
(a)
ad 50-70
b+
d 0-10
b(b)
os 0-inf
b-
Figure 6: Di erent template STGs that model the behavior of di erent delay-lines.
a+
0-inf 25-inf d s 25-inf d
5.1.2 Adding speci cation relations
a+
s
0-20 d 0-inf
b+
75-inf d
u+
b+
75-inf d
u+
50100 s d
50-70
s
50-100
d+
0-inf s d 0-20
a25-inf d s
au0-inf 25-inf d 0-inf s
u50-70 d
b-
b-
d(a) (b)
Figure 7: (a) An STG that is not time-consistent. (b) An STG made time-consistent by the addition of a delay-line represented by signal d. The reason to add delay-lines is clear. It is not always possible to transform a time-inconsistent STG into a timeconsistent STG by only adding delay arcs. An example is shown in Figure 7. The speci cation relation u+ (50;100) u? ?! cannot be satis ed by only adding output-delay arcs. So therefore the delay-line represented in Figure 6(a) has been added and the correct arcs have been added to satisfy that relation. The result is shown in Figure 7(b). In this case mindelay = 0 and maxdelay = 20. Signal u is the input for the delay-line. In Section 5.2 a procedure is presented that transforms a time-inconsistent STG into a time-consistent STG by adding output-delay arcs and/or delay-lines. A procedure is presented that tries to satisfy the speci cation relations. Assume that there is a speci cation relation (place) p between t' and t that is not satis ed. The procedure tries to satisfy this relation by adding delay arcs pointing to t0 . The added delay arc is assigned a minimum value mindelay and a maximum value maxdelay determined by the user. Now
5.1.3 Adding input-delay relations
The compiler may not add input-delay arcs to already existing signals, because it is not allowed to change the behavior of the environment. In particular situations however it may be necessary to add circuitry that does not consist of pure logic. Classical examples are delay-lines and arbitration circuits. In most practical cases the terminal behavior of these circuits can be modeled by an STG. So the behavior of the complete circuit (= logic circuit and special circuits) can be modeled in one STG. The special circuit, once it is added, is considered to be part of the environment. So its output signals are considered to be input signals for the synthesized logic circuit. Hence if the compiler wants to add special circuitry, input-delay arcs have to be added to the STG.
5.2 Transformations to satisfy the speci cation relations
every t00 , that can be used as a starting node for the delay arc, should satisfy the following relation: 8# 2 (Pd; S ) : #(t) + minf (p) #(t00 ) + mindelay #(t00 ) + maxdelay #(t) + maxf (p) (2) This can also be rewritten as minf (p) min(#(t00 ) ? #(t)) + mindelay # max(#(t00 ) ? #(t)) + maxdelay maxf (p) (3) # The above condition is a necessary and su cient condition to satisfy that particular speci cation relation. Other speci cation relations are not taken into account however. So after the transformation is performed, a timing analysis algorithm should check whether no speci cation relations that were initially satis ed, are now violated. If this is the case the transformation should be rejected. If there are more alternatives, it is a good strategy to take the transition t00 which has the lowest max# (#(t00 ) ? #(t)). This gives more freedom to the compiler to perform transformations afterwards. It is possible that no event t00 can be found that satis es relation 3. As explained above, such an event should be created by adding a delay-line. Assume that the delay-line has a (minline ; maxline ) characteristic. For the example of Figure 6(b) this is (50, 70). Signal s can serve as an input for the delay-line if this signal has a transition s that satis es the following condition. minf (p) min(#(s ) ? #(t)) + mindelay + minline # max(#(s ) ? #(t)) + maxdelay + maxline maxf (p) (4) # If a number of alternatives are available, it is a good approach to choose the solution with the smallest delay-line. Small delay-lines are usually more reliable than the bigger ones and consume less area. The global procedure then becomes as follows: Algorithm 1 (Making an STG time-consistent) MakeTimeConsistent ( S )
return
g
if ( ( 0S ; p) == 0) return NULL; /* no solution */ 0 S = S;
S;
g
The following algorithm tries to nd a signal transition for adding delay arcs. FindTriggerTransition returns a signal transition newt such that if a delay arc is added between newt and t the speci cation relation p may be satis ed.
Algorithm 2 FindTriggerTransition ( S ; p) f max = 1
g
newt = NULL; p is a place between t and t0 ; FOREACH (t00 2 T ) f 00 if(t satis es relations 3) if (max#(#(t00 ) ? #(t)) max) f max = max#(#(t00 ) ? #(t)); newt = t00 ; g g return newt;
For a discussion of the running time the reader is referred to 9].
For these transformations it is assumed that the initial STG from which the transformation process starts, is timeconsistent. So during the transformation process the compiler has to check after each transformation whether the STG is still time-consistent. If it is not time-consistent it means that the transformation, which the compiler has performed, is not a valid one. The compiler then searches for another transformation that results in a time-consistent STG. If no such transformation can be found, the compiler cannot nd a sof pset = ; /* the set of speci cation rel. already satis ed.*/ lution within the constraints and within the user estimate for the maxdelay and mindelay values. The user therefore has to FOREACH (p 2 Ps) adapt his estimation of maxdelay and mindelay values or he if( ( S ; p) == 1) pset = pset fpg; FOREACH (p 2 (Ps n pset)) /* p is not satis ed yet. */ may even be forced to change the initial speci cation. This process is schematically represented in Figure 4. f newt = FindtriggerTransition ( S ; p); 6 Case study if (newt == NULL) The initial timed STG for an up-down counter is shown in f FOREACH (delay-line in LIBRARY from small to big) Figure 8. There are two conditional paths: a goes high or b goes high rst. d1 and d2 represent the behavior of two f 0 delay-lines. Although this is a cyclic graph, the analysis and S = S + delay-line added;/* Section 5.1.3*/ synthesis can be performed on the two acyclic parts which /* See Equation 4. */ constitute this STG. newt = FindtriggerTransition ( 0S , p); This STG does not satisfy the CSC requirement. Therefore if (newt != NULL) a state signal has to be added using techniques presented in f 0 9]. With this example we want to demonstrate that di erent S = S; solutions will be found dependent on the choice of the delaybreak; max parameter. gg g if (newt == NULL) return NULL; /* no solution */ Assume that the user sets delay-max = 10 ns . Part of the 0 = S + delay arc added from newt to t0 ; resulting STG is presented in Figure 9(a). The implemenS pset = pset fpg; tation is shown in Figure 10(a). A new transition H + of a FOREACH (p 2 pset) state signal H has been added to resolve the state assignment
5.3 Transformations to satisfy the CSCrequirement
D2 B H
c c
down
0-inf s
b+
25-inf d 25-inf
a+
s 0-inf
D1 A H
D2 B up H D1 A down H down up A B
c
down
D2 H B up H D1 H A down H
c
down
up
c
up
down20-40 d
up20-40 d
d
down up A B
c
up
c
H
c (b)
H
a+ d2+
0-40 s 75-inf d
b+ d2+
75-inf d 0-40 s
down up A B
c (c)
H
(a)
down+
20-40 d
b25-inf d 25-inf
a-
up+
20-40
Figure 10: (a) Implementation of the STG in Figure 9 (a). (b) Implementation of the STG in Figure 9 (b). (c) Implementation of the STG in Figure 9 (c). In this paper, a number of extensions have been discussed to model time in the STG-model. Based on these new semantics a transformation technique is discussed to transform an STG in such a way that the circuit derived from the STG satis es all the speci ed timing constraints.
d
d
d20-inf s
d2ad d
b-
s
0-inf
7 Conclusions
75-inf
75-inf
Figure 8: (a) Initial timed STG for an up-down counter.
0-10 d
References
b+
25-inf d s
0-15 s
b+
25-inf d
0-24 d
b+
25-inf d
down- 0-10
20-40 d d
down- 0-15
20-40 d d
down- 0-24
20-40 d d
1] G. Borriello. \A New Interface Speci cation Methodology and Its Application to Transducer Synthesis". PhD thesis, U.C. Berkeley, 1988.
H+
s 0-inf
H+
s 0-inf s
H+
d s 0-inf
a+ d2+
75-inf d 0-15 d
a+ d2+
75-inf d 0-24 d
d2+
0-10 d
a+
75-inf d
2] S. M. Burns. Sizing asynchronous circuits produced by martin synthesis. In ACM International Workshop on Timing Issues in the Speci cation and Synthesis of Digital Systems, Aug. 1990. 3] T. A. Chu. Synthesis of Self-timed VLSI Circuits from Graphtheoretic Speci cations. PhD thesis, MIT, June 1987. 4] L. Lavagno, K. Keutzer, and A. Sangiovanni-Vincentelli. Algorithms for synthesis of hazard-free asynchronous circuits. In Proceedings of the Design Automation Conference, pages 302{308, June 1991. 5] K. McMillan and D. L. Dill. \Algorithms for Interface Timing Veri cation.". In 1992 ACM/SIGDA Workshop on Timing Issues in the Speci cation and Synthesis of Digital Systems., 1992. 6] C. Myers and T. Meng. Synthesis of timed asynchronous circuits. In Proceedings of the International Conference on Computer Design, pages 121 { 125, October 1992. 7] J. L. Peterson. \Petri Net Theory and the Modeling of Systems". Prentice-Hall, 1981. 8] T. Rokicki and C. Myers. Automatic veri cation of timed circuits. In CAV, 1994. 9] P. Vanbekbergen. Synthesis of Asynchronous Control Circuits from Graph-Theoretic speci cations. PhD thesis, Catholic University of Leuven, ESAT, Sept. 1993. 10] P. Vanbekbergen, G. Goossens, and H. D. Man. Speci cation and analysis of timing constraints in signal transition graphs. In Proceedings of the European Design Automation Conference, pages 302{306, March 1992. 11] P. Vanbekbergen, B. Lin, G. Goossens, and H. de Man. A generalized state assignment theory for transformations on signal transition graphs. In Proc. of the ICCAD, pp. 112{117, Nov. 1992. 12] V. I. Varshavsky. Self-timed Control of Concurrent Processes. Kluwer Academic Publisher, 1990. (Russian edition: 1986).
0-24
down+
b-
down+
b-
down+
b-
(a)
(b)
(c)
Figure 9: (a) Part of the transformed STG with delay-max = 10. (b) Part of the transformed STG with delay-max = 15. (c) Part of the transformed STG with delay-max = 24. con icts. For more information on satisfying state assignment con icts the reader is referred to 9]. Note that the new transition H + has been added in a very \strict" way. It is for instance speci ed that down should go low and next H should go high before a goes high. Dependent on the library this implementation might not satisfy these requirements. This can be veri ed with a timing veri er like the one presented in 8]. The user might therefore adapt his estimation for delay-max . Assume that the user now sets delay-max = 15 ns . Part of the resulting STG is presented in Figure 9(b). The implementation is shown in Figure 10(b). The transition H + now has been added in a less \strict" way. It can be veri ed now that the resultant logic becomes slightly more complex. If this implementation still does not satisfy all the requirements, the user can set delay-max = 24 ns . Part of the resulting STG is presented in Figure 9(c). The implementation is shown in Figure 10(c). Again the resultant logic becomes slightly more complex. If this implementation still does not satisfy the assumptions, the user is forced to change the speci cation or to take another library of gates.