Asynchronous interface specification, analysis and synthesis

Asynchronous Interface Specification, Analysis and Synthesis  Michael Kishinevsky Jordi Cortadella Intel Corporation Technical University of Catalonia Hillsboro, OR, USA Barcelona, Spain Alex Kondratyev Luciano Lavagno The University of Aizu Politecnico di Torino Aizu-Wakamatsu, Japan Torino, Italy Abstract Interfaces, by nature, are often asynchronous since they serve for connecting multiple distributed modules/agents without common clock. However, recent development in theory of asynchronous design in the area of asynchronous specifications and models, analysis and verification, synthesis and technology mapping, timing optimization and performance analysis is not widely known and rarely accepted by industry. The goal of this tutorial is to fill this gap and to present an overview of one popular systematic design methodology for design of asynchronous interface controllers. This methodology is based on using Petri nets (PN)a formal model that, from the engineering standpoint, is a formalization of timing diagrams (waveforms) and from the system designer standpoint is a concurrent state machine, in which local components can perform independent or interdependent concurrent actions, changing their local states asynchronously. We will introduce this model informally based on a simple example: a VME-bus controller serving reads from a device to a bus and writes from the bus into the device. 1 Specification with Petri Nets Let us start with introducing the Petri Nets specifications with a simple example. 1.1 From timing diagrams to PNs Figure 1 depicts the interface of a device with a VME bus. The behavior of the controller is as follows: a request to read from or write into the device is received by one of the signals DS r or  Work partially supported by ACiD-WG (Esprit 21949) and CICYT TIC 95-0419 DSr DSw DTACK LDS LDTACK Device VME Bus Controller D Transceiver Data Bus Figure 1: VME bus controller DSr LDS LDTACK D DTACK Figure 2: Waveforms for the READ cycle DS w respectively. In a read cycle, a request to read is done through signal LD S . When the device has the data ready ( LD T AC K ), the controller must open the transceiver to transfer data to the bus (signal D ). In the write cycle, data is first transferred to the device. Next, a request to write is done ( LD S ). Once the device acknowledges the reception of the data ( LD T AC K ) the transceiver must be closed to isolate the device from the bus. Each transaction must be completed by a return-tozero of all interface signals, seeking for a maximum parallelism between the bus and the device operations. Figure 2 shows a timing diagram of the read cycle and Figure 3 the corresponding to its Marked Graph – a simple class of Petri nets, in which only concurrency and sequencing, but not choice is allowed. All events in this Marked Graph are interpreted as signal transitions: rising and falling signal transitions are labeled with “ + ” and “ ; ” respectively. Petri Nets with such signal interpretations are called Signal Transition Graphs (or STGs) [16]. APN has two types of vertices: places (denoted by circles) and transitions (denoted by boxes), and arcs from places to transitions and from transitions to places. Places correspond to local states of the system and are used for keeping information about system resources and conditions for execution of transitions. Places can keep tokens (denoted by black dots). A token in a place indicates that a resource is available or a condition satisfied. In general more than one token can be kept in a place, but we will consider only the simplest case: place can contain not more than LDS+ LDTACK+ DSr+ LDTACK - D+ DTACKLDSDTACK+ DDSrp0 p1 p2p3 p6 p7 p8 p9 p10 p5 p4 Figure 3: STG for the READ cycle one token (so-called safe or 1-bounded PNs). A set of all places currently marked with a token corresponds to a current global state of the net. Such global states are called markings. The initial marking of the PN in Figure 3 is f p 0 p 1 g . 1.2 Token game Transitions correspond to system events (signal transitionsin the example). A transition is enabled if all input places contain a token. In the initial marking of the PN in Figure 3 only one transition, DS r + , is enabled; another one, LD S + , is not: only place p 1 among two of its input places, p 1 and p 2 , contains a token. Every enabled transition can fire. Firing removes one token from every input place of the transition and puts one token to each of its output places. Firing of a transition is an atomic instantaneous operation, while some unspecified time can pass between enabling and firing of the transition. After the firing of transition DS r + the net moves to a new marking f p 1 p 2 g and then LD S + becomes enabled, etc. 1.3 Concurrency This process of moving tokens around (a.k.a. token game) in a few steps will fire transition D ; . This leads the net into the marking f p 7 p 8 g . In this marking two transitions D T AC K ; and LD S ; become enabled. Since their input places are different they do not conflict for tokens and cannot disable each other. This represents concurrency between DT AC K ; and LD S ; . In total, there are four pairs of concurrent transitions: ( DT AC K ; LDS ; ) , ( D T AC K ;  LD T AC K ; ) , DSr+ LDS+ DTACKLDTACK+ LDTACKD+ LDSLDTACKDSr+ DTACK+ LDTACKDTACK-DSr+ LDSLDS-DTACKDSrD- {p0,p1} {p1,p2} {p3} {p4} {p6} {p9} {p10} {p7,p8} {p0,p8} {p2,p8} {p2,p5} {p0,p5} {p5,p7} {p1,p7} 01*.11*.0 0*0.11*.0 10.11*.0 10.11.0* 10.0*1.0 10.1*0.0 10.00*.0 0*0.00.0 01*.00.0 01*.1*0.0 00.1*0.0 01.11.1* 1*1.11.1 <DSr,DTACK,LDTACK,LDS,D> 10*.11.1 Figure 4: RG and SG for the READ cycle ( DS r + LDS ; ) , and ( DS r +  LD T AC K ; ) , where concurrency is a potential to fire at the same time. 1.4 State graphs Playing the token game one can generate a Transition System (TS)– an abstract state graph in which each arc between a pair of states is labeled with the corresponding fired transition. Figure 4 depicts a TS for the READ cycle if we ignore for a moment labels associated with states 1 . Each state in the TS generated from a PN corresponds to a marking, which is shown at the left from the corresponding state. A TS with states labeled with markings is called a reachability graph of a PN. For Signal Transition Graphs each state of the corresponding TS also can be associated with a binary code of signal values, which are shownat the right from the states (for the sake of readability we separate with dots left handshake signals, right handshake signals, and data transceiver control signal; enabled signals are marked with an asterisk). A TS with states labeled with binary codes of signals is called a state graph of an STG. State graphs are of primary importance since they form the basis of logic synthesis for asynchronous logic netlist. 1.5 Choice and arbitration The environment of the device has a choice to request the read or the write operation. Similarly, if an arbitration within the device is involved, then the device itself can internally make a non1 States are denoted with circles. Initial state is marked with a dot. DSr+DSw+ LDS+D+ DTACKLDTACK+ LDS+ D+ DTACK+ DSrDLDSDSwLDTACKDTACK+ DLDTACK+ p0 p1 p2 p3 Figure 5: STG for READ and WRITE cycles deterministic choice between two requests. Choice is expressed in PNs by choice places as shown in Figure 5. Here places p 0 and p 3 are choice places, places p 1 and p 2 merge alternativebranches of the behavior and all other places are removed from the figure, since they have only one input and one output arc (they are called implicitplaces and are represented by arcs between two transitions). In the initial marking f p 0 p 3 g two input transitions are enabled – DS w + and DS r + , but as soon as one of them fires another becomes disabled, since the token will disappear from place p 0 . 1.6 Timing extensions Different timing extensions have been proposed to PNs to express (a) assumptions about delays and (b) deadline requirements. This information could come in a form of absolute values, e.g.  min max ] delay intervals associated with transitions or places, or in the form of relative informa- tion, like ”transition a will (or must) fire before transition b ”. 2 Analysis and verification 2.1 Properties Analysis and verification are used at different stages of design.  Property verification. After specifying the design it is required to check implementability properties to answer the following question: ”Can the specification be implemented with an asynchronous circuit?” [13, 15]. Other properties of the specification can be of interest as well, e.g., absence of deadlocks, fairness in serving requests, etc. General purpose verification techniques can be employed for this analysis [18].  Implementation verification. After design is done fully automatically or (especially) with some manual intervention it is often desirable to check that the implementation is correct with respect to the given specification [10, 23].  Performance analysis and separation between events is required (a) for determining latency and throughput of the device and (b) for logic optimizationbased on timing information [12, 21] (see also Section 5). Properties required for implementability include:  boundedness of the PN to guarantee that the specified state space is finite;  consistency of an STG to ensure that rising and falling transitions alternate for each signal;  completeness of state encoding to check that there are no conflicts in definition of Boolean functions for each non-input (i.e. output and internal) signals;  persistency of the STG to verify that (a) no non-input signal transition can be disabled by another signal transition and (b) no input signal transition can be disabled by a non-input signal transition. The former ensures that no short glitches, known as hazards, can appear at the gate outputs, while the latter ensures that no hazards can occur at inputs of the device. If all the above properties are satisfied, then the STG specification can be implemented as a, so-called, speed-independent circuit [19] 2 . Speed-independence means no hazards under any variations of gate delays if variations of some critical wire delays after forks (so-called isochronic forks) stay within reasonable bounds (e.g., within one gate delay). Let us illustrate two of the above properties with an example. Two states in the TS in Figure 4 are underlined. They correspond to the different markings, f p 4 g and f p 2 p 8 g , but their binary codes are equal, 10110 . Moreover, enabling conditions in these two states for output signals LD S , and D are different. Therefore, the implied value of the nextstate Boolean function for signal LD S for vector 10110 should be 1 (for the first state) and 0 (for the second state). This is a conflict in 2 Also called quasi-delay-insensitive in the literature [17, 2] the definition of the function. To resolve this conflict two methods can be employed: (a) inserting an additional state signal whose value should distinguish two conflict states or (b) concurrency reduction. In the first case one feasible solution is to insert rising transition of the additional state signal right before LD S + and its falling transition right before D ; . So conflicting states will be associated with different values of the new state signal. In the second case, a possible solution is to remove the conflicting state f p 2 p 8 g from the specification. The environment should usually stay untouched for the compositional reasons, therefore delaying input signals is not allowed. Hence, signal transition DT AC K ; can be delayed until LD S ; fires. The automatic techniques for solving the state encoding problem are presented, e.g., in [6, 26]. To illustrate the persistency property let us consider transitions DS w + and DS r + in Figure 5 assuming for a moment that they are output signals to be implemented. Both are simultaneously enabled and disable each other after firing. Such behavior cannot be implemented without hazards unless special mutual exclusion elements (arbiters) are used. 2.2 Techniques There are several techniques for fighting with the “state explosion problem” in analysis of Petri Net-like specifications.  Symbolic Binary Decision Diagram-based (BDD) [3] traversal of a reachability graph allows its implicit representation which is generally much more compact than an explicit enumeration of states [23].  Partial order reductions ( [11], stubborn sets [25], identification method [13]) ignores many (or even most) of the states for analysis of certain properties.  Structural properties of PNs (e.g., place invariants) can provide fast upper approximation of the reachability space [20, 9] and also can be used for dense variable encoding of states in the reachability graph. Structural reductions are useful as a preprocessing step in order to simplify the structure of the net before traversal or analysis, keeping all importantproperties.  Unfoldings [18, 15] are finite acyclic prefixes of the PN behavior, representing all reachable markings. They are often more compact than the reachability graph and due to the acyclic property are well-suited for extracting ordering relations between places and transitions (concurrency, conflict and preceding). Different types of unfoldings are also used for performance analysis [12]. Figure 6 is a result of applying linear reductions to the STG from Figure 5. Using more elaborate reductions (place and transition fusions) it is possible to reduce the whole PN from Figure 3 to a single self-loop transition [20]. The BDD-based method used for deriving the transition function and calculating the reachable markings of a PN are similar to those used for reachability analysis and equivalence checking of finite state machines: starting from the initial marking by iterative application of the transition function the characteristic function of the reachability set is calculated until the fixed point is reached. However, the naive encoding, one Boolean variable per place, can be too costly for large designs. 0 0 1 1 00 00 00 11 11 11 0 0 0 1 1 1 00 00 00 00 11 11 11 11 0 0 0 0 1 1 1 1 00 00 00 00 00 11 11 11 11 11 0 0 0 1 1 1 00000 00000 00000 00000 00000 11111 11111 11111 11111 11111 0 0 0 0 1 1 1 1 0 0 0 1 1 1 000 000 000 000 111 111 111 111 B DCA F p5 p1 p4 p0 00 00 11 11 0 0 0 0 1 1 1 1 00 00 00 11 11 11 00 00 00 11 11 11 p2 p3 E 0 0 1 1 00 00 00 11 11 11 0 0 0 1 1 1 00 00 00 00 11 11 11 11 0 0 0 0 1 1 1 1 00 00 00 00 00 11 11 11 11 11 0 0 0 1 1 1 00000 00000 00000 00000 00000 11111 11111 11111 11111 11111 000 000 000 000 111 111 111 111 B DCA F p5 p1 p4 p0 00 00 00 11 11 11 00 00 00 11 11 11 00 00 00 11 11 11 p2 p3 E 00 00 00 11 11 11 0 0 0 1 1 1 00 00 00 11 11 11 p5 D B Figure 6: STG after liner reduction and two state machine components The following observation can be made: the sets of places P 0 = f p 2 p 3 p 5 g and P 1 = f p 0 p 1 p 4 p 5 g of the PN in Figure 6 define two state machines [20, 9] with the following sets of transitions T 0 = f B D E g and T 1 = f A B  C  D  F g , respectively. This information can be structurally obtained by using algebraic methods. State machines (see the Figure) correspond to place-invariants of the PN and preserve their token count in all reachable markings. Therefore, the following are two invariants for the net: I 1 ( p 2 p 3 p 5 ): p 2 + p 3 + p 5 = 1 I 2 ( p 0 p 1 p 4 p 5 ): p 0 + p 1 + p 4 + p 5 = 1 If invariants I 1 ( p 2 p 3 p 5 ) and I 2 ( p 0 p 1 p 4 p 5 ) are represented as Boolean functions (e.g., using BDD), then the AND operation on these two functions will give us for this example an exact characteristic function of the reachability set of markings. In general a conjunction of any set of invariants gives an upper approximation of the reachability set, which is useful for conservative verification. On the other hand, due to the invariants above, the following dense encoding for places can be proposed: place v 0 v 1 v 2 v 3  p p 2 00-- v 0 v 1 p 3 01-- v 0 v 1 p 5 1--- v 1 p 0 --00 v 2 v 3 p 1 --01 v 2 v 3 p 4 --1v 2 p 5 ---- - Then, the characteristic function of the reachability set is reduced to a constant: R ( V )= v 0 v 1 ( v 2 + v 2 )+ v 0 v 1 ( v 2 + v 2 )+ v 0  1 : DSr+ csc0+ DTACKLDS+ LDTACKLDTACK+ LDTACKDSr+LDSLDTACKDTACK-LDS-DSr+ D+ LDS-DTACKDTACK+ DDSrcsc0100000* 0*00000 100*101 1000*01 10110*1 10*1111 1*11111 011111* 01111*0 01*11*00 01*1*000 0*011*00 1011*00 101*000 0*01*000 01*0000 <DSr,DTACK,LDTACK,LDS,D,csc0> Figure 7: SG for the READ cycle with complete state coding. 3 Logic Synthesis The goal of logic synthesis is to derive a gate netlist that implements the behavior defined by the specification. For simplicity, we willillustrate thisstep by synthesizinga speed-independent circuit for the read cycle of the VME bus (see Figure 3). The main steps in logic synthesis are the following:  Encode the SG in such a way that the complete state coding property holds. This may require the addition of internal signals.  Derive the next-state functions for each output and internal signal of the circuit.  Map the functions onto a netlist of gates. 3.1 Complete State Coding As mentioned in Section 2.1, the SGof Figure 4 has state conflicts. A possible method to solvethis problem is to insert new state signals that disambiguate the encoding conflicts. Figure 7 depicts a new SG in which a new signal, csc0, has been inserted. Now, the next-state functions for signals LD S and D can be uniquely defined. The insertion of new signals must be done in such a way that the resulting SG preserves the properties for implementability. [4] S. Burns. General conditions for the decomposition of state holding elements. In International Symposium on Advanced Research in Asynchronous Circuits and Systems, Aizu, Japan, March 1996. [5] J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, E. Pastor, and A. Yakovlev. Decomposition and technology mapping of speed-independent circuits using boolean relations. In Proceedings of the International Conference on Computer-Aided Design, pages 220–227, November 1997. [6] J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, and A. Yakovlev. A region-based theory for state assignment in speed-independent circuits. IEEE Transactions on Computer-Aided Design, 16(8):793–812, August 1997. [7] J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, and A. Yakovlev. Synthesis of control circuits from STG specifications. In handouts of the Summer School on Asynchronous Circuit Design, August 1997. http://www.lsi.upc.es/˜jordic/petrify/refs/summer97.ps.gz. [8] J. Cortadella, M. Kishinevsky, L. Lavagno, and A. Yakovlev. Synthesizing Petri nets from state-based models. In Proceedings of the International Conference on Computer-Aided Design, pages 164–171, November 1995. [9] J. Desel and J. Esparza. Free-choice Petri Nets, volume 40 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1995. [10] David L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. MIT Press, 1989. [11] P. Godefroid. Using partial orders to improve automatic verification methods. In E.M Clarke and R.P. Kurshan, editors, Proc. International Workshop on Computer Aided Verification, 1990. DIMACS Series in Discrete Mathematica and Theoretical Computer Science, 1991, pages 321-340. [12] H. Hulgaard, S. M. Burns, T. Amon, and G. Borriello. An algorithm for exact bounds on the time separation of events in concurrenct systems. IEEE Transactions on Computers, 44(11):1306–1317, November 1995. [13] M. A. Kishinevsky, A. Y. Kondratyev, A. R. Taubin, and V. I. Varshavsky. Concurrent Hardware. The Theory and Practice of Self-Timed Design. John Wiley and Sons Ltd., 1994. [14] A. Kondratyev, M. Kishinevsky, B. Lin, P. Vanbekbergen, and A. Yakovlev. Basic gate implementation of speed-independent circuits. In Proceedings of the Design Automation Conference, pages 56–62, June 1994. [15] A. Kondratyev, M. Kishinevsky, A. Taubin, and S. Ten. Analysis of Petri nets by ordering relations in reduced unfoldings. Formal Methods in System Design, 12(1):5–38, 1997. [16] L. Lavagno and A. Sangiovanni-Vincentelli. Algorithms for synthesis and testing of asynchronous circuits. Kluwer Academic Publishers, 1993. [17] A. Martin. Programming in VLSI: From communicating processes to delay-insensitive circuits. In C. A. R. Hoare, editor, Developments in Concurrency and Communications, The UT Year of Programming Series. Addison-Wesley, 1990. [18] K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. [19] David E. Muller and W. S. Bartky. A theory of asynchronous circuits. In Proceedings of an International Symposium on the Theory of Switching, pages 204–243. Harvard University Press, April 1959. [20] T. Murata. Petri Nets: Properties, analysis and applications. Proceedings of the IEEE, pages 541–580, April 1989. [21] Chris J. Myers and Teresa H.-Y. Meng. Synthesis of timed asynchronous circuits. IEEE Transactions on VLSI Systems, 1(2):106–119, June 1993. [22] Steven M. Nowick and David L. Dill. Exact two-level minimization of hazard-free logic with multipleinput changes. IEEE Transactions on Computer-Aided Design, 14(8):986–997, August 1995. [23] Oriol Roig, Jordi Cortadella, and Enric Pastor. Verification of asynchronous circuits by BDD-based model checking of Petri nets. In 16th International Conference on the Application and Theory of Petri Nets, volume 815 of Lecture Notes in Computer Science, pages 374–391, 1995. [24] S. H. Unger. Asynchronous Sequential Switching Circuits. Wiley-Interscience, John Wiley & Sons, Inc., New York, 1969. [25] Antti Valmari. Stubborn sets for reduced state space generation. Lecture Notes in Computer Science; Advances in Petri Nets 1990, 483:491–515, 1991. [26] P. Vanbekbergen, B. Lin, G. Goossens, and H. De Man. A generalized state assignment theory for transformations on Signal Transition Graphs. Journal of VLSI Signal Processing, 7(1-2):101–116, 1994. [27] Peter Vanbekbergen, Albert Wand, and Kurt Keutzer. A design and validation system for asynchronous circuits. In Proc. ACM/IEEE Design Automation Conference, June 1995. [28] K. Y. Yun and D. L. Dill. Automatic synthesis of 3D asynchronous state machines. In Proceedings of the International Conference on Computer-Aided Design, November 1992.