Structural methods for the synthesis of speed-independent circuits

1108 IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 17, NO. 11, NOVEMBER 1998 Structural Methods for the Synthesis of Speed-Independent Circuits Enric Pastor, Jordi Cortadella, Member, IEEE, Alex Kondratyev, Member, IEEE, and Oriol Roig Abstract—Asynchronous circuits can be modeled as concurrent systems in which events are interpreted as signal transitions. The synthesis of concurrent systems implies the analysis of a vast state space that often requires computationally expensive methods. This work presents new methods for the synthesis of speed-independent circuits from a new perspective, overcoming both the analysis and computation complexity bottlenecks. The circuits are specified by free-choice signal transition graphs (STG’s), a subclass of interpreted Petri nets. The synthesis approach is divided into the following steps: correctness, binary coding, implementability conditions, and logic synthesis. Each step is efficiently implemented by applying a set of structural techniques that analyze STG’s without explicitly enumerating the underlying state space. Experimental results show that circuits can be generated from specifications that exceed in several orders of magnitude the largest STG’s ever synthesized—with over 10 27 states. Computation times are also dramatically reduced. Nevertheless, the quality of results does not suffer from the use of structural techniques. Index Terms— Asynchronous circuits, Petri nets, speedindependent synthesis. I. INTRODUCTION ASYNCHRONOUS circuits promise a number of important advantages for the design of large digital circuits. Their modularity, potential low-power consumption, averagecase computation time, and elimination of the clock distribution problem have encouraged their extensive analysis. However, any asynchronous implementation must satisfy much more restrictive conditions than its synchronous counterpart. Asynchronous circuits must be not only functionally equivalent to the specification but also free of hazards—undesired switching activity due to the skew of gate delays. Speed-independent circuits (SI circuits) is a broadly used design style for asynchronous implementations. SI circuits rely on the unbounded gate delay model, which assumes unknown but finite delays on the gates, and skew at the wires bounded by the delay of the fastest gate. Thus, the correctness of the circuit requires the assumption that some wire forks are Manuscript received November 13, 1997; revised March 30, 1998. This work was supported in part by CICYT under Grant TIC98-0410. This paper was recommended by Associate Editor A. Saldanha. E. Pastor is with the Department of Computer Architecture, Universitat Polit´ecnica de Catalunya, Barcelona 08034 Spain (e-mail: [email protected]). J. Cortadella is with the Department of Software, Universitat Polit´ ecnica de Catalunya, Barcelona 08034 Spain (e-mail: [email protected]). A. Kondratyev is with the Computer Architecture Laboratory, University of Aizu, Aizu-Wakamatsu 965 Japan (e-mail: [email protected]). O. Roig is with National Semiconductor Corp., Santa Clara, CA 95052 USA (e-mail: [email protected]). Publisher Item Identifier S 0278-0070(98)08591-1. isochronic [1]. SI circuits are robust to parameter variations, i.e., the response time of an SI circuit subjected to temperature or voltage modifications may vary, but the circuit keeps working correctly. Additionally, an SI circuit does not need any modification to guarantee its correctness after a technology migration (the validity of isochronic forks must be checked, however). The most robust delay model, delay-insensitive circuits, also assumes unbounded wire delays. Unfortunately, the class of delay-insensitive circuits is very small from the practical point of view [1]. A wide range of synthesis techniques for asynchronous circuits rely on event-based models, such as Petri nets (PN’s) [2] or change diagrams [3]. PN’s are a powerful formalism to model concurrent systems that gracefully captures the notions of causality, concurrency, and conflict between events. As a model, their most interesting feature is the capability of implicitly describing a vast state space by a succinct representation. Hence, PN’s have been chosen by many authors as a formalism to describe the behavior of asynchronous circuits by interpreting the events as signal transitions, thus coining the term signal transition graph (STG) [4], [5]. Each reachable marking of an STG has assigned a binary vector with the value of the circuit signals in that marking. Deriving logic equations from an STG requires the generation of the binary codes for all markings. Currently, most synthesis tools [6]–[8] perform an exhaustive token flow analysis to obtain the complete reachability graph of the PN and all binary vectors. Unfortunately, the reachability graph of highly concurrent systems can be exponential in the size of the STG that leads to the well-known state explosion problem. Some efforts have been devoted to propose structural methods for synthesis [9], [10], but they have been usually devised for restricted classes of PN’s that compromise the potential expressiveness of this formalism. This work presents a structural methodology for the synthesis of SI circuits from STG’s. The proposed techniques have polynomial complexity if the underlying PN is free choice [11], [12], and can be efficiently extended to the class of PN’s that can be covered by state machines [13]. The proposed structural techniques are based on the analysis of the concurrency relations of STG’s [5], and the generation of covering cubes that approximate the reachable markings. Additional information obtained from the state machines of the STG allows one to refine the initial covering cubes, increasing the accuracy of the approximations. This methodology eliminates the state explosion problem by avoiding the explicit generation of all the markings in the STG. Even though 0278–0070/98$10.00 1998 IEEE PASTOR et al.: SYNTHESIS OF SPEED-INDEPENDENT CIRCUITS 1109 the concurrency relations have been previously applied for synthesis [10], [14], this work generalizes the use of these relations, reducing the gap between structural and state-based approaches. We aim at complementing the existing tools by providing alternative and efficient synthesis algorithms for state-machinecoverable STG’s, which account for a large number of STG’s used for circuit design. The area and delay results of the SI circuits synthesized by applying our method are presented and compared with those obtained by previous synthesis tools. This paper is organized as follows. The formal notions on Petri nets and signal transition graphs are presented in Section II. The implementability conditions of speedindependent circuits are analyzed in Section III. Section IV illustrates the structural synthesis framework and its efficiency by means of two examples. To avoid the state explosion problem, Section V proposes a method to derive approximations of the reachability graph from the structure of the STG. Section VI describes how Boolean functions can be obtained from these approximations. A strategy to increase the accuracy of such approximations is introduced in Section VII. The overall logic-minimization framework is described in Section VIII, and further minimizations are outlined in the Appendix. Several experimental results and efficiency analysis are presented in Section IX. Section X concludes this paper. II. BASIC NOTIONS AND DEFINITIONS In this section, we briefly recall some of the basic definitions on logic functions, Petri nets, and signal transition graphs. For more detailed information on these topics, we refer the reader to [5], [12], and [15]–[17]. A. Logic Functions An incompletely specified -variable logic function is a mapping . Each element is called a vertex. The set of vertices where evaluates to 1, 0, and are called on-, off-, and dc-sets and are denoted by on ,off , and dc , respectively. A literal is either a variable or its complement .Acube c is a set of literals such that if , then , and vice versa. Cubes can also be represented as an element , in which value “0” denotes a complemented variable , value “1” denotes a variable , and indicates that the variable is not in the cube. A cover is a set of implicants that contains the on-set and does not intersect with the off-set. B. Petri Nets and STG’s A PN is a four-tuple , where is the set of places, is the set of transitions, is the flow relation, and is the initial marking. Given a node , its postset and preset are denoted by and , respectively. A marking of a PN is an assignment of a nonnegative integer to each place. If is assigned to place by marking , we will say that is marked with tokens, i.e., .Apath in a PN is a sequence of nodes such that . A path is called simple if no node appears more than once on it. A state machine (SM) is a PN such that each transition has exactly one input place and one output place. A free choice (FC) net is a PN such that every arc from a place is either a unique outgoing arc or a unique incoming arc to a transition. A transition is enabled in a marking , denoted by , when all places in are marked. An enabled transition in fires, removing one token from each place in and adding one token to every place in . This produces a new marking ( ). A marking is reachable from if there is a sequence of firings that transforms into ( ); hence is a feasible sequence. The set of reachable markings from is denoted by . The graphical representation of a reachability set with the vertices corresponding to markings and arcs corresponding to transitions between markings is called a reachability graph (RG). Two transitions and are concurrent if there exists a marking in which both transitions are enabled and the firing of or does not disable the other. APNislive if every transition can be infinitely enabled through some feasible sequence of firings from any marking in . A PN is safe if no marking in can assign more than one token to any place. A place is redundant if its removal preserves the set of feasible sequences in the PN. In the sequel, we will assume that all the considered PN’s are free choice, live,safe, and do not contain redundant places.1 A PN can be decomposed into a potentially exponential set of strongly connected state machines, also named SMcomponents (SM’s) [11]. In particular, live and safe freechoice PN’s are covered by one-token SM’s; that is, SM’s that contain exactly one token [11]. Computing SM’s is reduced to solving a linear programming model, with polynomial complexity [18]. An SM-cover (SMC) is a subset of onetoken SM’s such that every place in a PN is included at least in one SM. An STG is a triple , where is its underlying PN, is a set of input and output signals, and is a labeling function , in which the transitions are interpreted as value changes on circuit signals. Rising and falling transitions of a signal are denoted by and , respectively, while denotes a generic rising or falling transition. Multiple transitions for a signal will be distinguished by means of indexes, e.g., . (In figures, instead of indexes for , will be used.) An STG is autoconcurrent if it contains a pair of concurrent transitions of the same signal. An STG is graphically represented as a directed graph with transitions denoted by their names and places by circles, where places that have only one transition in its preset and postset are usually omitted. Also, transitions of input signals are underlined. Fig. 1(a) depicts a free-choice STG, taken from [19], that will be used throughout this work. The example contains input ( ) and output ( ) signals. The corresponding reachability graph of the STG is depicted in Fig. 1(b). Fig. 2 depicts three SM’s that cover the STG. 1Checking for liveness, safeness, and redundant places can be done in polynomial time for FC nets [12]. 1110 IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 17, NO. 11, NOVEMBER 1998 (a) (b) Fig. 1. (a) STG example and (b) corresponding reachability graph. Fig. 2. SM-components of example depicted in Fig. 1(a). Each marking of an STG is encoded with a binary code of signal values by means of a labeling function , where denotes the binary value for signal . The function must consistently encode the STG markings; that is, no marking can have an enabled rising (falling) transition if .In a nonautoconcurrent STG, transition is a predecessor of if there exists a feasible sequence that does not include other transitions of signal . Conversely, is a successor of —we will also say that the pair is adjacent. The set of predecessors (successors) of is denoted by prev (next . In Fig. 1(b), transition has two successor transitions and , while at the same time is a single predecessor to both rising transitions. An STG is called output semimodular if no output signal transition enabled at any reachable marking can be disabled by the transition of another signal [20]. If an STG is output semimodular, then it can be implemented without producing unspecified changes of the output signals; that is, without introducing hazards. C. Signal Regions To derive the correspondence among the signal transitions, the reachable markings, and the properties of the specification, different signal regions are defined. PASTOR et al.: SYNTHESIS OF SPEED-INDEPENDENT CIRCUITS 1111 TABLE I SIGNAL REGIONS FOR THE EXAMPLE IN FIG.1 The excitation region ER is the set of markings in which transition is enabled. It can be shown that, for live and safe free-choice STG, excitation regions are connected sets of markings. The quiescent region QR is the maximal set of markings that are reached from ER after firing without enabling any other transition . The restricted quiescent region QR is the subset of the quiescent region QR that does not contain markings of other QR’s of signal . The generalized rising (falling) excitation region of signal is the union of all excitation regions ER ER , denoted by GER and GER . The generalized one (zero) quiescent region of is the union of all quiescent regions QR QR , and it is denoted by GQR GQR . Fig. 1(b) depicts the excitation regions ER ,ER ,ER for the output signal . Regions are collections of markings; hence, we use the operator to define the characteristic function of the binary codes of the markings in a set or region. Additionally, we will define the dc-set as the set of nonused binary codes, i.e., . Examples of other regions and binary codes for signal can be found in Table I. D. State Coding An STG is said to satisfy the complete state coding (CSC) property if, when the same binary code is assigned to two different markings, the output signals enabled at both markings are identical, i.e., . An efficient technique to verify the CSC property can be derived if instead of analyzing individual markings, the encoding properties are checked in terms of sets of markings related to the structure of the STG, i.e., GER GQR GER GQR . A more restrictive property, the unique state coding (USC) condition, holds if all reachable markings of the STG are assigned a unique binary code, i.e., . The example in Fig. 1 has a USC conflict because markings and share the binary code (1111). However, the STG satisfies the CSC property because output transition is enabled at neither nor (i.e., no CSC conflict exists). E. Next-State Function The derivation of a circuit that implements the behavior specified by an STG consists in finding a logic-gate realization of the next-state function for each output signal. The next-state function, , of a signal is defined as follows [21]: if GER GQR if GER GQR otherwise. For any STG that fulfills the consistency and CSC conditions, is consistently defined, i.e., on off dc is a complete partition of . Note that for any pair of output signals and ,dc dc DC, where DC denotes the dc-set of the reachability graph. An implementation of the next-state function by a cover is correct if on on DC (1) III. SPEED-INDEPENDENCE SYNTHESIS CONDITIONS The derivation of an SI circuit from an STG specification requires two types of correctness conditions [20]. •Specification correctness conditions: Consistency, output semimodularity, and CSC. These conditions have been defined in Section II and guarantee that a correct SI circuit can be derived from the STG specification. •Implementation correctness conditions: These conditions guarantee that a given circuit implements the desired behavior. We can distinguish two types of conditions. — Correct next-state function condition (1). — Conditions for hazard freeness, which depend on the specific circuit architecture chosen for the implementation. These conditions will be discussed in Section III-B. Consistency and CSC are necessary and sufficient conditions for the existence of a consistent next-state function. Output semimodularity is a necessary condition for the existence of a hazard-free implementation of the behavior. In the case where all next-state functions can be correctly implemented by a hazard-free complex gate, the circuit is guaranteed to be SI [5]. The implementability conditions of SI circuits have been exhaustively investigated in [7], [17], [19], and [22]. However, it is not always possible to implement each nextstate function with one complex gate. In general, gate libraries impose constraints on the size and functionality of the logic functions that can be implemented with only one gate. This section first introduces three different implementation architectures and discusses sufficient conditions for obtaining correct implementations of the next-state functions. It is shown that these conditions can be formulated in terms of requirements for the covers of the corresponding signal regions. The rest of the section is devoted to discussing the conditions for hazard freeness that guarantee the synthesis of an SI circuit. One of the architectures is chosen for the illustration of the methodology of structural synthesis throughout the paper. However, the suggested methods are easily adapted to other architecture styles as well. A. Implementation Architectures 1) Atomic Complex Gate Per Signal: This is the initial architecture for SI circuits studied in [5] and [23]. The circuit 1112 IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 17, NO. 11, NOVEMBER 1998 Fig. 3. Implementation architectures. is implemented as a network of atomic gates, each one implementing one output signal. The Boolean function for each gate can be represented as a sum of products (SOP). A simple example of such gate is presented in Fig. 3(a). Each atomic gate contains a combinational part and a possibly sequential part implemented as an internal feedback. The delay between its “ANDing” and “ORing” nodes and the internal feedback is assumed to be negligible. In the figures, the gate representation is used to denote the implemented logic function, but the actual implementation is resolved on the transistor level. The circuit is assumed to be derived by building a correct cover for [according to (1)] and implemented by a single complex gate. It was shown in [5] that for correct STG’s, this equation gives necessary and sufficient conditions for the speed independence of the implementation (i.e., no additional architecture-specific conditions are needed). However, the requirement to implement each cover by a single gate might be quite unrealistic in practice, which is the weakest point for this approach. 2) Atomic Complex Gate Per Excitation Function: This architecture was suggested and studied extensively in a number of papers, e.g., [20] and [24]. It assumes that a separate memory element is used to produce an output signal. The set and reset excitation functions for signal are fed to the memory element. They are implemented as atomic complex gates. Fig. 3(b) shows an example of such architecture with a C-latch used as a memory element. Sufficient conditions that guarantee the implementation correctness of the next-state function are the following: GER on GER off (2) The set function for signal must be turned on every time some rising transition is enabled and turned off before the enabling of any falling transition ; similarly for the reset function. However, the conditions in (2) do not guarantee an SI circuit. Sufficient extra conditions for hazard freeness will be discussed in Section III-B. It is possible to show the existence of an implementation in this architecture for any STG satisfying the CSC condition [5]. Fig. 4. Three speed-independent implementations for signal d . 3) Atomic Complex Gate Per Excitation Region: Signals in this architecture are created using networks of atomic complex gates to implement the set and reset functions of the memory element. Each transition is implemented by a single gate, which is then connected to an OR-gate whose output is in turn fed into the memory element. As a result, smaller complex gates are used. The basic structure of this architecture is shown in Fig. 3(c). In this architecture, every gate at the first level of the set function implements the behavior of a single rising transition . This gate must be turned on every time transition is enabled and turned off before the enabling of any falling transition ; similarly for the reset function. In a nonautoconcurrent STG, only one transition of the signal can be enabled at a certain instant. Therefore, the proposed architecture evolves under a one-hot encoding discipline of the gates at the first level of the set and reset networks. Only one of the gates can be “ON” at the same time, being responsible for the output signal to switch. The rising and falling signal switching is produced due to the alternate activation of set and reset networks. The implementation correctness condition for the covers is similar to condition (2) but is limited to only use its excitation and quiescent region ER ER QR DC (3) The detailed discussion on the sufficient conditions to ensure an SI implementation with this architecture can found in [7] and [19]. A general discussion on these conditions is presented in Section III-B. Fig. 4 shows the implementations of signal from the STG in Fig. 1 in all three architectures. More recent developments aim at the decomposition of complex gates used to implement each excitation region. The goal of these techniques is to guarantee the implementability of the circuit in a particular gate library or with a network of two-input gates [25], [26]. From the review of the possible architectures, we can conclude that the architecture-specific conditions for correct implementations can always be formulated in terms of covering the signal regions. In Section VI, it will be shown how to obtain approximations for each signal region by using the information contained in the structure of the STG rather than its RG. Therefore, the synthesis techniques suggested in PASTOR et al.: SYNTHESIS OF SPEED-INDEPENDENT CIRCUITS 1113 (a) (b) (c) Fig. 5. (a) STG and covering cubes for places, (b) reachability graph, and (c) refined covers. this work can be adapted to any implementation architecture. Further, we will illustrate the synthesis method in application to the architecture in Fig. 3(b), when the set and reset functions are implemented as atomic complex gates. Note, however, that there are no strict borders between different architecture styles and, for optimization purposes, we can easily admit the implementation of one signal of a circuit as an atomic complex gate while the other is implemented by the set and reset networks. These issues are mainly addressed in Section VIII, where the circuit minimization loop is discussed. B. Conditions for Hazard Freeness In the previous section, we introduced three main types of implementation architectures and formulated the conditions that must be satisfied by Boolean functions of gates to ensure the proper values of implemented signals. However, this functional correctness is not sufficient to guarantee the hazardfree behavior of a circuit. Even when the Boolean functions of gates are defined according to the requirements of Section IIIA, the behavior of the circuit can be hazardous due to the delays in the propagation of signals through the gates. This must be avoided in speed-independent designs. In this section, we introduce the sufficient conditions that will capture the absence of hazards during the operation of a circuit. From now on, unless it is pointed out explicitly, we assume that each output signal of the STG is implemented by complex gates for set and reset functions—atomic complex gate per excitation function—with a C-latch as memory element. The correctness of the set and reset covers is not sufficient to guarantee the SI behavior of the implementations. Additionally, these covers must be monotonic. Intuitively, is said to be monotonic if it changes exactly twice in any sequence of firing transitions, rising at a marking in GER GER and falling either inside GQR GQR or before entering GER GER . For example, (see Fig. 1), assume that covers markings and . is correct, but if the circuit follows the sequence , it might produce an undesired glitch at function that might eventually be propagated to output . The following property describes how the set and reset covers can be verified to be monotonic exploring the reachable markings of the STG rather than its feasible firing sequences. Property 1 [Monotonic Covers]: A set function is said to be monotonic iff GQR such that its code is covered by , then GQR , the binary code is also covered by . A reset function is said to be monotonic iff GQR such that its code is covered by , then GQR , the binary code is also covered by . For the particular case of the atomic complex gate per excitation region architecture, each cover must satisfy an additional monotonic condition designed to guarantee a hazard-free alternating one-hot activation of set and reset networks. A cover cannot freely use its QR as dc-set because some of its markings may be shared by other covers for signal . In Fig. 1, marking is shared in the QR’s of both transitions and . If the cover includes that shared marking, both covers and will be incorrectly excited (not necessarily at the same time) whenever transition is expected to be fired. The additional condition to guarantee the monotonic alternating activation of set and reset networks can be expressed by using the restricted quiescent region as ER ER QR DC (4) Imposing restrictions on the markings that can be covered to guarantee the one-hot enabling discipline is equivalent to the single entrance constraint described by other authors [7], [24]. However, in order to verify this restriction, restricted quiescent regions are easier to build and structurally characterize than firing sequences. The result proved in [7] and [19] is the following: “If the correct set and reset covers satisfy the monotonicity conditions, the circuit implementation is speed independent.” The main purpose of the following sections is to show how the correctness and monotonicity conditions can be ensured for the set and reset covers without generating the reachability graph of the STG. IV. APPLYING STRUCTURAL METHODS TO SYNTHESIS This section gives an intuitive picture of the proposed structural methods by using the example depicted in Fig. 5(a). The techniques here described are fundamental to support the overall synthesis process keeping its complexity polynomial. 1114 IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 17, NO. 11, NOVEMBER 1998 (a) (b) (c) Fig. 6. Signal insertion. (a) STG and covering cubes for places, (b) reachability graph, and (c) implementation for signal y . Let us assume that we wish to derive a logic function to cover the excitation region of [denoted ER ]. This region corresponds to the set of markings in which place is marked. The encoded reachability graph obtained from the STG is depicted in Fig. 5(b), in which ER is also shadowed. By a simple structural analysis that takes polynomial time [12], we can deduce that the STG has an underlying freechoice PN in which each SM has exactly one token. We can also derive a set of SM’s that cover the net (SM-cover). In this case, two SM’s can be obtained, namely, the sets of nodes SM and SM . Our purpose is to calculate a set of cubes that safely cover ER .2An initial single cube approximation can be calculated as follows. If a signal transition can fire while a given place is marked, without removing the token from the place, then the value of the signal is unknown while the place is marked. Since transitions and can fire when is marked, then the value of and is unknown in . On the contrary, the value of can be exactly determined by analyzing the ordering relation of and with . Thus, the cube can be derived for . However, we can easily detect that this cube is an overestimation of ER because the binary code which is outside ER is also covered. Assuming to be a cover cube for ER leads to the erroneous conclusion on the enabling of in . Note that overestimation does not necessarily happen in the approximation process: for places and , the cubes can be exactly calculated, i.e., and , respectively. To fight with the possible overestimations, two strategies can be applied. 1) Cover refinement: Refining the place covers by analyzing the concurrent relations with other places. To obtain a multicube approximation, we use the fact that can only be simultaneously marked with ,,or . The 2ER ( y +) is the set of binary codes of markings in ER ( y +) . The cover must contain ER ( y +) (on-set) and may contain codes from the dc-set. cover of should be intersected with the conjunction of the covers of , , and [see Fig. 5(c)]. Then, the function (10 ) ( 01) correctly covers ER [see Fig. 6(c)]. Note that, in general, several refinements may be needed. 2) Signal insertion: Inserting state signals in the same way as solving encoding conflicts, disambiguating covers whose intersection produces contradictions for synthesis. This is illustrated in Fig. 6, in which a new signal distinguishes the covers of and . Then, the cube correctly covers ER [see Fig. 6(c)]. In general, both methods can be combined to obtain a correct set of covers. In this work, we only present the conditions under which a set of covers can be safely used for synthesis without the insertion of extra signals. The procedures for insertion of extra signals are covered in [27]. To give an intuitive idea about the efficiency of the structural approach, let us consider one illustrative example. Fig. 7 presents an autonomous circuit with a C-latch closed on its inputs through inverters. A C-latch is the basic cell used for the synchronization of processes in asynchronous designs. Its output rises when all its inputs are “1” and falls when all inputs are “0”; in any other case the output remains unchanged. The logic function for a C-latch is . In our example, a change on the output of the C-latch leads to a concurrent burst of input changes. The number of markings in an -input circuit is , while the number of places in the corresponding STG is only . The use of cover cubes for the places in this example is extremely efficient because they exactly define the excitation regions for all signal transitions; that is, the information provided by the concurrency relations coincides with the structure of the reachability graph. Given transition , the cube of its predecessor place is an exact cover for ER (signal order is used). Given transition , the intersection of cubes for its predecessor places , , and gives the single code (1110) where is enabled . PASTOR et al.: SYNTHESIS OF SPEED-INDEPENDENT CIRCUITS 1115 (a) (b) Fig. 7. (a) Generalized-latch circuit and (b) its STG specification. In this example, we have obtained the functions for signals from the structural information in the STG rather than by restoration of its reachability graph. Although the function derivation procedure is not always so simple, it allows one to present a general view of complexity reduction while using the cover cube approximations. In the rest of this paper, we describe the conditions to determine how the aforementioned covers can be iteratively improved and when the reached accuracy is sufficient to be considered correct. V. STG STRUCTURAL ANALYSIS This section presents structural methods for analyzing STG’s [28]. This method will be used in Section VI to find approximate covers for ER’s and QR’s. ER’s and QR’s will be approximated by a much simpler region that characterizes the markings in which a given place is marked, the so-called marked region. The goal of this section is to derive a single cube cover for each marked region by using a set of structural properties that can be computed in polynomial time on the size of the STG. Based on the concurrency relations and the analysis of paths in the PN, we introduce a polynomial algorithm to verify the consistency of the STG. Consistency is a necessary condition for the synthesis of SI circuits, but it is also necessary to guarantee the existence of a consistent next-state function for the signals in the STG. Using the concurrency and the interleaving between signals, cubes will be derived to approximate the binary codes of markings in the marked regions. A. Concurrency Relations The concurrency relation (CR) [5] is a conservative concept defined in terms of markings in the RG of an STG that provides a high-level view of its dynamic behavior. When two transitions can fire from a marking without disabling each other, the transitions are said to be concurrent. Since this is a structural property, its definition must be conservative. Two transitions may appear to be concurrent in one part of the RG TABLE II SCR BETWEEN SIGNALS AND PLACES FOR THE STG IN FIG.1 while ordered in another. In that case, we should take them as concurrent because they are not always ordered. Concurrency relations can be extended to places and signals [27]. We will refer to the formalization of concurrency between nodes and signals as signal concurrency relations (SCR). Definition 2 (Concurrency Relations): The concurrency relation between pairs of nodes of an STG is defined as a binary relation such that given places , transitions , exists Definition 3 (Signal Concurrency Relations): The signal concurrency relation between a node and a signal is defined as a binary relation such that . Polynomial algorithms for the computation of the concurrency relations of a live and safe free-choice PN have been presented in [29]. As an example, Table II depicts the ’s for the places of STG in Fig. 1(a) [where indicates those pairs that are concurrent]. B. Consistency Verification If an STG is not consistent, it cannot be implemented by a logic circuit. Therefore, consistency must be checked before performing the synthesis step. This section presents an efficient algorithm to verify the consistency of a live, safe, and irredundant free-choice STG by using the concurrency relations and the structure of the underlying PN. 1116 IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 17, NO. 11, NOVEMBER 1998 An STG satisfies the consistency condition if it does not contain autoconcurrent transitions and every sequence of signal transitions is switchover correct [20]. To avoid autoconcurrent transitions, no pair and of transitions of the same signal is allowed to be simultaneously enabled at the same marking. Switchover correctness requires the value of each signal to switch from zero to one in response to a rising transition and from one to zero due to a falling transition. Nonautoconcurrency can be structurally verified by using the signal concurrency relations, i.e., by checking that each transition is nonconcurrent with signal . The switchover correctness of a nonautoconcurrent STG can be verified by checking that all adjacent transitions of the same signal have alternating switching directions. A pair of transitions of the same signal can be determined to be adjacent by finding a particular path in the STG connecting both transitions. The following property characterizes the relation between the formal definition of adjacency on the RG and its efficient computation on the structure of the STG. Property 4 (Structural Characterization of Adjacency) [Necessary Condition]: In a live and free-choice STG, a transition next if there is a simple path between and such that: 1) no place is concurrent to signal ; 2) contains no other transitions of signal except and . Proof: The proof is done by induction on the length of the path . (The length of the path is always odd.) 1) . Then (where denote arcs between STG nodes). If is a choice place, then it is free choice and the sequence is feasible. If is not a choice place, then the token in can be consumed only by transition . From the liveness of the STG, it follows that there exists a feasible sequence that contains both and . Suppose that in any such sequence there is some other transition between and . Clearly, is concurrent to any transition between and , and so it is concurrent to , which contradicts the initial assumption. Therefore, next . 2) From the statement’s being true for , it follows that it is also true for . Consider the last transition before , i.e., . The path between and has length , and by the induction assumption, there exists feasible sequence such that does not contain any transition of signal . Let us show that can be extended as , where contains no transitions of signal . This clearly follows from the consideration of item 1) for , and therefore, next . Assuming that an STG is nonautoconcurrent, Property 4 provides the necessary conditions to check whether is adjacent to . To derive the sufficient conditions, we need to introduce several additional notions. A path starting at and ending at is called realizable by a feasible sequence if the sequence includes all transitions in . The reason to introduce the (a) (b) Fig. 8. STG showing (a) insufficiency of Property 4 and (b) nonconsistently interleaved place p k . realizable paths is to restrict the number of simple paths to be analyzed when constructing the set next . Actually, it is sufficient to consider only those simple paths that are realizable by , where contains no transition of signal . The necessary conditions that characterize the paths between adjacent transitions of the same signal (given by Property 4) require any place in the path to be nonconcurrent to all transitions of the considered signal. This condition is not sufficient, as can be seen from the example in Fig. 8(a). In this STG, the sequence is feasible, and therefore next . However, place is concurrent to , and the only simple path between and goes through . To obtain sufficient conditions for the adjacency between transitions of the same signal, it is necessary to distinguish which concurrency relations are not relevant for adjacency. This analysis can be done on the basis of forward reduction by concurrent transitions. Informally, forward reduction of PN by a set of transitions is obtained by removing from all the nodes starting from that cannot be reached without the firing of some transition . We will denote the resulting PN via . The forward reduction can be obtained by the following procedure: Remove transitions from do until a fixed-point in modifying is reached if for all transitions have been removed then remove from if has been removed then remove all . The mechanism of forward reduction allows one to formulate the sufficient conditions for the existence of a realizable path between pairs of adjacent transitions of the same signal. Property 5 (Characterization of Adjacency) [Sufficient Condition]: In a nonautoconcurrent, free-choice STG ,if next , then there exists a simple path between and such that: PASTOR et al.: SYNTHESIS OF SPEED-INDEPENDENT CIRCUITS 1123 Fig. 12. Cover function marking coding refinement algorithm. ; which means that place should have a structural coding conflict in every SM-component (see Property 7). (The motivation for this fact is that any reachable marking should be included in some marked region.) Conversely, if SM contains place but does not contain any other place for which , then we can conclude that is not a reachable marking, and the structural coding conflict between and is fake (happens only due to an overestimation of ) [27], [30]. Additionally, it can be guaranteed that the SM-component SM can be used to effectively refine the cover function of place and eliminate the overestimation. Since no place SM has a structural conflict with , no cover cube in SM covers . The refinement for is computed SM , and after the refinement, the cover function does not have structural coding conflicts in SM . The procedure depicted in Fig. 12 refines the cover functions of places in the STG when fake structural conflicts are detected. Note that refinements concern not only the place with structural conflicts but all the places in the STG. This is done because we found that in practice, places closer to other places with fake structural conflicts have also overestimated cover functions. Even though the overestimation could be in the dc-set, our experiments show that this more general application of refinement leads to much better minimization solutions. The example in Fig. 1(a) contains three structural coding conflicts at SM (Fig. 2) Places and do not have structural coding conflicts at SM . Therefore, this SM-component can be used to refine the corresponding cover functions The technique for the resolving the structural conflict between and is different and is discussed further. 2) Refinement Technique and CSC Property: Refinement does not work if the structural coding conflict for places and (in Fig. 1) corresponds to reachable markings and MR MR . However, the correctness of the cover [see (2)] is not violated if a coding conflict corresponds to markings and that satisfy the CSC property. The structure of the STG provides a sufficient condition to find whether the structural coding conflict satisfies the CSC property. Theorem 14 (Sufficient Condition for CSC): If an STG has a CSC violation, then in a given SM-cover SMC, one can find an SM-component SM containing a pair of places and such that: 1) is in the preset of an output transition ; 2) is not in the preset of any other transition of signal ; 3) ER MR . Proof: A CSC violation means that there exists an output signal such that ER and ER . Let us assume that is the first transition of signal that can be enabled in a feasible sequence starting from , i.e., and no other transition of signal is enabled in . Since ER , there is at least one place that is not marked in . Let us take an SM-component SM including place . According to the STG liveness, and should hold a token in places and , respectively ( SM, where is an input place to ). Clearly, by the choice of , place cannot be in a preset of any transition , and Condition 2) of the theorem is satisfied. Taking into account that ER ER and MR , we can conclude that ER MR . Theorem 15 (Detection of Fake Coding Conflicts): An STG satisfies the CSC property if for any place in the preset of an output signal transition , there exists an SM-component SM in the SMC including place such that SM does not contain any structural coding conflict for ; i.e., : SM SMC SM SM MR MR . Proof: Let us assume the existence of a CSC violation due to markings and . From Theorem 14, there should exist an SM-component SM SMC containing two places , , and a transition such that and ER , MR , but MR . We will prove that if there exists SM SMC that contain both nodes and without coding conflicts for place , then the assumed CSC violation is contradicted. Since MR , there should exist a place SM such that MR . Hence, a coding conflict should exist between places and . But place does not contain any coding conflict in SM , which contradicts the assumption about the CSC violation. Both Theorems 14 and 15 provide the conditions to eliminate structural coding conflicts in specifications that satisfy the CSC condition. Let us go back to the structural coding conflict between places at SM of the STG in Fig. 1(a). This coding conflict cannot be eliminated by means of refinement because place has the same coding conflict at SM , and a coding conflict at SM . However, the conflict between places and satisfies Theorem 14. Note that and ; therefore, if it would correspond to a real CSC conflict, there would exist some other place not in the preset of any transition of signal holding a conflict with place . Since that is not the case, this conflict can be related to markings that satisfy the CSC condition. Last, it can be concluded that place has no conflicts and SM can 1124 IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 17, NO. 11, NOVEMBER 1998 be used to determine that the conflict between and is fake at both SM and SM . VIII. SYNTHESIS METHODOLOGY This section completes the synthesis process by applying the signal region approximations to the design of an SIcircuit under a particular architecture. For simplicity, we have selected the atomic complex gate per excitation function architecture. This work proposes a two-step heuristic synthesis algorithm. Initially, nonoptimized set and reset excitation functions that satisfy the implementability conditions (correctness and monotonicity) are derived. Starting from these covers, several minimizations are applied to simplify the functions while maintaining the implementability conditions. However, every time minimization is applied, the algorithm must determine whether the final result is speed independence or not. Therefore, both correctness and monotonicity should be structurally verified before accepting the minimization. A. Initial Excitation Functions The set and reset functions for a signal must cover all binary codes in its rising and falling generalized excitation regions. Since markings in GER’s are obtained by combining the particular ER’s, set and reset covers can be computed as the union of covers for transitions, i.e., and . Property 13 guarantees that under the absence of structural conflicts, the cover functions are correct covers for ER ; therefore, and . Following Theorem 15, a cover cube does not overestimate ER if no predecessor place needs refinement. Structural coding conflicts are checked in the SM-cover. If they exist, refining or inserting state signals is necessary. The absence of structural coding conflicts guarantees the CSC property [27] and the existence of correct covers. By applying this scheme to signal in Fig. 1, we obtain . As place , corresponding to , is involved in a structural conflict, its cover cube is refined into a set of binary codes . Place , corresponding to ,is free of structural conflicts, and its cover cube does not need any refinement. As a result, . Similarly, we can obtain . B. Checking the Synthesis Conditions From the initial set of covers, multiple minimization techniques will be tried in order to simplify the final implementation. Some of these transformations can be directly applied without further correctness or monotonicity checking because they are known to preserve these properties. However, any minimization technique that implies increasing the number of markings covered by the set/reset covers requires checking the SI synthesis conditions to guarantee the speed independence of the result. 1) Correctness: The correctness condition [see (2)] requires all binary codes of markings in GER GER to be covered by . This condition defines the on-set on of the function and can be verified as: , and . Also, no binary code of markings inside GER GQR GER GQR can be used in the minimization of . This condition defines the off-set off of the function, and can be verified as: QPS , and QPS . 2) Monotonicity: The monotonicity condition has to be checked for each cover by using a two-step technique. To simplify the reasoning, let us assume that contains exactly one cube. Assuming the correctness of the cover , it implies that the cube will be turned on at ER but should be turned off somewhere inside QR or before reaching the following ER’s. Then, it cannot be turned on again inside the quiescent region without violating the monotonicity condition; that is, the cover can only be switched on to implement transition (see Definition 1). The monotonicity condition can be structurally verified by determining the border places in QPS in which the cover cube still can be ON, while in their successors it should be turned OFF. Let us define as the set of transitions in [where next ] that will turn off for the first time. Let us also generalize the interleaving relation for the pairs and , where . To guarantee the monotonicity condition, given any place in QPS that is interleaved in ( is reached after ), the intersection between the cover and the cover function should be empty. This is characterized formally in the following property. Property 16 (Structural Checking of Monotonicity): The correct cover is monotonic if for any next any and any place , the cover does not intersect with . Proof: If a cover is correct (2), then has to be turned off somewhere inside QPS . By examining the transitions that are in [where next ], we can find the set of transitions turning off for the first time. Note that none of the literals corresponding to transitions before reaching can be present in the cube . To be monotonic, once is turned off by a transition in , the cube cannot be turned on again inside QPS . The marked region of all sequences of places that are in is covered by . Conversely, all places that are in can be reached only after the firing of ; that is, after the cube is turned off. Therefore, monotonicity is ensured if cube is never turned on again in the markings that are covered by the marked regions of places . As an example, let us assume that we have computed the cover for the STG in Fig. 1. The set will contain transitions ; therefore, is monotonic because it can intersect with the covers PASTOR et al.: SYNTHESIS OF SPEED-INDEPENDENT CIRCUITS 1125 for place but cannot intersect with the covers of any place interleaved between and . When has several cubes, the monotonic sequences defined by the set are conservatively computed. A transition belongs to the set if it is the first one such that the cover cubes of the places in its postset are not completely covered by , i.e., QPS . C. Synthesis Algorithm From the initial set of covers, several minimizations are heuristically applied. (A detailed description of each minimization is described in the Appendix.) For simplicity, we assume that the STG satisfies the CSC condition; otherwise, state encoding techniques are applied [30]. Additionally, safeness, liveness, and consistency on the STG should be checked beforehand [12], [31]. The selected minimization process is the following. 1) Each set/reset cover is expanded toward the quiescent regions and dc-set by eliminating literals. 2) After expansion toward the quiescent region, covers are checked to be complete; that is, if the set (reset) cover includes all binary codes in GQR GQR , then the atomic complex gate per signal architecture can be used, hence avoiding the use of a C-latch. 3) Signals that cannot be directly implemented by the set or reset cover, i.e., requiring the memory element, can be further expanded toward the quiescent region of its predecessor transitions (see the Appendix). 4) The C-latch can be collapsed with the set and reset covers, leading to a potential simplification of the circuit. 5) The overall synthesis process is completed by creating the circuit and mapping its different elements onto a gate library. To demonstrate the evolution of the covers through the minimization process, the synthesis algorithm will be applied to the output signal in Fig. 1. The previously computed initial covers are , , , and in the first step of the minimization process are expanded toward the quiescent region and dc-set. Literal can be eliminated from the support of including markings in the cover, which results in . Literal can be eliminated from both and , generating the cover . When simplifying the cover , literal can be eliminated, expanding the cover toward the dc-set, which results in . Last, literal can be eliminated from , obtaining . Both covers are used to implement the set function . With respect to , literal can be eliminated by expanding the cover toward the quiescent region and obtaining . For this particular signal, complete cover minimization nor backward expansion nor memory collapsing can be applied. The final implementation is depicted in Fig. 4(b). IX. EXPERIMENTAL RESULTS This section presents a number of experiments that evaluate the quality of the proposed synthesis methodology. Four relevant issues have been analyzed: 1) the influence of minimization on the final area of circuits, 2) area results compared to previous synthesis methodologies, 3) CPU speedup due to the structural algorithm compared to state-based algorithms, and 4) the relation among markings in the STG’s, the number of cubes required for the structural approximations, and the quality of area minimizations. Note that all synthesis results have been formally verified to be speed independent [32]. The CPU times have been obtained on a Sun SPARC20 workstation. In all tables, columns labeled , , and indicate the number of places, transitions, and reachable markings. Columns labeled and SM denote the number of cubes and SM’s required by structural algorithms. These values give an intuitive idea about the complexity of each benchmark. A. Heuristics for Area Minimization This section compares the average area improvement obtained in two benchmark sets (see Fig. 13). In both cases, the process starts from an initial semioptimized implementation, in which only expansions toward the quiescent region and dcset have been applied, and progressively evolves toward more efficient implementations. Points in the column labeled are the initial semioptimized implementation. Progressively, in column , transitions are allowed to be merged; in ,complete signal networks are detected. Memory element collapsing is applied at . Last, region covers are expanded toward the backward quiescent regions in (see the Appendix). From a technologyindependent implementation, a Boolean-matching mapping algorithm is applied [33]. The column labeled presents the results obtained after the application of a technologymapping step that, for example, merges simple gates into complex ones when available in the library (currently complex gates up to four inputs such as AOI22). B. Area of the Circuits Table V compares the area results of several synthesis tools including our methodology. The goal of this experiment is to show that even though structural techniques only approximate the reachable markings in the STG’s, this methodology does not negatively influence the quality of the circuits. Columns labeled SYN and FCG report the area obtained by the synthesis methodologies developed at Stanford [24] and Aizu [19]. Columns labeled S3C contain area results for our methodology without using the backward minimization and mapping (left column) and fully minimized (right column). The results show that the new logic-minimization techniques provide significant improvements—23% area reduction with respect to [24]—in short CPU times—less than 8 s for the worst case (pe-send-ifc). We also took into account that some of the new minimization techniques were not fully 1126 IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 17, NO. 11, NOVEMBER 1998 Fig. 13. Average minimization results for the benchmark sets. TABLE V AREA RESULTS COMPARISON WITH TOTALS BY SYN (1) AND BY FORCAGE (2) ( 3 NONFREE-CHOICE—NONAVAILABLE RESULT) used by SYN and FORCAGE (e.g., backward expansions and mapping). Thus, for the sake of comparison fairness, we disabled such optimizations, still obtaining a 15% improvement. Therefore, we can conclude from the experimental results that structural methods, even being conservative, do not influence negatively on the quality of the final result. C. CPU Time: Structural Versus State Based To illustrate the effectiveness of structural over state-graphbased methods, we have run some experiments for STG’s with a large reachability graph, comparing CPU times with SIS [6] and ASSASSIN [8] (see Table VI). The superiority of structural methods is evident. Table VII reports the CPU times for two large scalable benchmarks. The dining philosophers benchmark is one of the examples that illustrates that nonfree-choice STG’s can also be synthesized if a cover of state machines can be found for the net. Another scalable example is the Muller pipeline. Its STG contains no choice places, and the circuit realization is a chain of C-latches. TABLE VI CPU TIME FOR SYNTHESIS:COMPARISON WITH SIS AND ASSASSIN D. Efficiency of the Cube Approximations We have analyzed the efficiency of approximating the binary codes of a reachability graph by sets of cubes. This is achieved by comparing the number of required cubes versus the number of nodes in the STG and the number of reachable markings versus the number cubes. The cube comparison is done separately for two classes of STG’s, those with PASTOR et al.: SYNTHESIS OF SPEED-INDEPENDENT CIRCUITS 1127 TABLE VII CPU TIME FOR SYNTHESIS:SCALABLE EXAMPLES ( 3 NON-FC STG’s) TABLE VIII TRADEOFFS AMONG MARKINGS,NODES,AND CUBES less than 10 markings and those surpassing this limit (see Table VIII). For small benchmarks, we have reached a cubes/node ratio closer to 2.4, while the markings/cube ratio is closer to 1.7. Therefore, we can conclude that for small STG’s, there are no significant differences between using the reachability graph or the proposed structural techniques. On the other hand, for larger benchmarks, the cubes/node ratio is closer to 2.6, while the markings/cube ratio is closer to 4 10 . Thus, each node requires 2.6 cubes, and each cube approximates up to 410 markings—therefore justifying the efficiency of the cover-approximations methodology. X. CONCLUSIONS Structural techniques for the analysis and synthesis of STG’s are essential when the size of the state space becomes unmanageable. The proposed structural techniques intend to fill the gap between the STG’s that can be analyzed by current state-based techniques and the existing STG’s specifications of complex systems. This work has presented new methods to synthesize STG’s whose underlying PN is free choice. The proposed algorithms have polynomial complexity in the size of the net and can be easily extended to the class of PN’s that can be covered by SM-components, although the existence of a SM-cover cannot be guaranteed for any nonfree-choice Petri net. The experimental results show that the proposed methods obtain area-efficient implementations in short CPU times. Most of the existing tools were unable to synthesize the largest circuits, whereas the presented method is able to do it in few seconds. Future work will be devoted to fully characterize the class of Petri nets that can be handled by the presented techniques. APPENDIX MINIMIZATION TECHNIQUES This Appendix will provide an overview of the minimization techniques that are structurally applied to simplify the covers used in an atomic complex gate per excitation region architecture. A. Basic Concepts To efficiently implement this architecture, output signal transitions are partitioned into sets of transition clusters [34], [35]. Each cluster implies a complex gate for its implementation. These complex gates are combined by OR to form the set and reset functions, respectively. Definition 17 (Transition Cluster): We define the transition clusters as a total partition of the rising and falling transitions of one output signal , which must satisfy the following conditions. 1) Every rising or falling cluster contains at least one transition. 2) Every rising (falling) transition must be in one and only one transition cluster strictly composed of other rising (falling) transitions of the same signal. A transition cluster, whether or not it contains rising or falling transitions, will be simply denoted by . Superscripts are used to differentiate clusters of the same signal. All signal region definitions (ER’s, QR’s, QR , etc.) and implementability conditions can be easily extended to the usage on transition clusters. Fig. 4(b) and (c) shows two different implementations for output signal in Fig. 1. The first implementation [Fig. 4(b)] corresponds to the transition cluster partitioning , , and , which are implemented by covers , , and . This circuit is not SI because if the AND-OR gate for is slow enough, the pulse on input can propagate to the output . In Fig. 4(c), transitions and are merged into one cluster . This makes the overall circuit simpler and SI (the races between inputs and take place only within one AND–OR gate). B. Complete Region Covers Generating complete covers for all the rising or falling transitions of an output signal is one of the efficient minimization techniques that can be applied. In that case, the circuit can be exclusively created by using the corresponding set or reset function [5]. Every cover is checked to be complete by analyzing that all markings in QR are covered by . If all rising covers are complete, the set function implements the circuit. Similarly, if all falling covers are complete, the reset function can be alternatively used. In case both rising and falling functions are complete, the smallest or faster function should be selected. C. Region Expansions Circuits can be minimized by expanding the region covers toward the quiescent region and the dc-set. All transformations are characterized by either the elimination of a signal from the support of the function or the elimination of literals from the cubes. The main objective of expanding is to simplify the covers but also to obtain complete region covers with the subsequent minimization (allows a combinational implementa- 1128 IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 17, NO. 11, NOVEMBER 1998 tion for the signal). Therefore, this minimization has a higher priority than other transformations. Transition clusters are merged together when the complexity of the resulting region cover decreases. Transition clusters and are merged, creating a new cluster with covers , and eliminating the seminal ones. Merging requires checking whenever the resulting cover can be positively matched in the gate library. Merging also allows one to derive an increased number of complete covers. D. Collapsing of Memory Elements The structure of the architecture and the behavior of the Clatch can be used to further simplify the circuit [24]. Consider the signal network for an output signal implemented by a C-latch with equation , and set and reset networks with one region cover each . Both cubes can be collapsed into the C-latch: , obtaining . Hence, both set and reset region networks can be substituted by , being and . Similarly, if the set and reset networks , their cubes have the same support and are at distance one. Again, both cubes can be collapsed into the C-latch, obtaining . Then, both set and reset region networks can be substituted by the expressions , being and the data and control inputs of a gated latch that replaces the initial C-latch. E. Backward Region Expansions The backward quiescent region BR of a transition is the maximal connected set of markings that can reach ER without enabling any other transition . Further circuit minimizations can be obtained if a cover is also extended to cover markings in its backward quiescent region BR . Covering markings in the backward quiescent regions is only possible because of the characteristics of the C-latch (as pointed out by [19] and [36]). Maintaining one of the inputs of the C-latch at 1 (0) while its output is at 1 (0) creates and extra observability dc-set that can be used to further minimize circuits. Given the architecture in Fig. 3(c), if both the set cover and the output are still at 1, activating the reset cover will not produce a falling transition of the output until the set cover falls to 0. Hence, the cover of any falling transition can be activated before reaching its ER, but only if it can be guaranteed that the set cover will remain at 1 until the falling transition is excited. Similar conditions apply for rising transitions. Similar monotonicity conditions are required in the backward regions; that is, the cover changes exactly twice in any sequence, where the rising change is at a marking in BR ER and the falling change in QR . The backward quiescent region BR can be structurally defined by the backward quiescent place set BPS .A place belongs to BPS if it is interleaved between and next , i.e., BPS next . The same concept can be extended to transition clusters and to restricted regions, i.e., BPS BPS . Last, it is also essential to determine which are the markings that the predecessor transition clusters are covering to determine the subset of the BR region that is allowed to be covered. For each place in BPS , we will define by the subset of markings in MR covered by some predecessor transition : QPS BPS . Once we have computed these subsets, the correct covering of markings in the backward quiescent region is straightforward: BPS . F. Technology Mapping Circuits generated after the overall minimization process are mapped onto the technology provided by the designer. Blocks in the signal network can be combined in single cells when available in the library of existing gates. This cellbinding process provides an extra degree of minimization by substituting several logic blocks in the signal network by a more efficiently implemented cell in the library. A technology mapper tailored for SI-circuits has been developed following the Boolean matching techniques proposed in [33]. However, note that it is not possible to apply a generalized decomposition process of the blocks in the signal network due to the restrictive correctness conditions imposed by speedindependent circuits [37]. REFERENCES [1] A. J. Martin, “Formal program transformations for VLSI circuit synthesis,” in Formal Development of Programs and Proofs, E. W. Dijkstra, Ed. Reading, MA: Addison-Wesley, 1989, pp. 59–80. [2] C. A. Petri, “Kommunikation mit Automaten,” Ph.D. dissertation, Institut f¨ ur Instrumentelle Mathematik, Bonn, 1962, Tech. Rep. Schriften des IIM Nr. 3. [3] M. A. Kishinevsky, A. Y. Kondratyev, and A. R. Taubin, “Formal method for self-timed design,” in Proc. Eur. Design Automation Conf., Feb. 1991, pp. 197–201. [4] L. Y. Rosenblum and A. V. Yakovlev, “Signal graphs: From self-timed to timed ones,” in Proc. Int. Workshop Timed Petri Nets, July 1985, pp. 199–206. [5] T.-A. Chu, “Synthesis of self-timed VLSI circuits from graph-theoretic specifications,” Ph.D. dissertation, Massachusetts Institute of Technology, Cambridge, June 1987. [6] E. M. Sentovich, K. J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P. R. Stephan, R. K. Brayton, and A. SangiovanniVincentelli, “SIS: A system for sequential circuits synthesis,” University of California, Berkeley/ERL, Tech. Rep. M92/41, May 1992. [7] P. A. Beerel and T. H. Meng, “Automatic gate-level synthesis of speedindependent circuits,” in Proc. IEEE/ACM Int. Conf. Computer Aided Design, IEEE Computer Society Press, Nov. 1992, pp. 581–586. [8] C. Ykman-Couvreur, B. Lin, and H. De Man, “ASSASSIN: A synthesis system for asynchronous control circuits,” IMEC, Sept. 1994, Tech. Rep., user and tutorial manual. [9] K.-J. Lin and C.-S. Lin, “Automatic synthesis of asynchronous circuits,” in Proc. ACM/IEEE Design Automation Conf., IEEE Computer Society Press, June 1991, pp. 296–301. [10] C. Ykman-Couvreur, B. Lin, G. Goossens, and H. De Man, “Synthesis and optimization of asynchronous controllers based on extended lock graph theory,” in Proc. Eur. Conf. Design Automation (EDAC), Feb. 1993, pp. 512–517. [11] M. Hack, “Analysis of production schemata by Petri nets,” M.S. thesis, Massachusetts Institute of Technology, Cambridge, Feb. 1972. PASTOR et al.: SYNTHESIS OF SPEED-INDEPENDENT CIRCUITS 1129 [12] J. Desel and J. Esparza, Free Choice Petri Nets. Cambridge, U.K.: Cambridge Univ. Press, 1995. [13] F. Garc´ıa-Vall´es and J. M. Colom, “A Boolean approach to the state machine decomposition of Petri nets with OBDD’s,” in Proc. 1995 IEEE Int. Conf. Systems, Man and Cybernetics, Oct. 1995. [14] P. Vanbekbergen, “Optimized synthesis of asynchronous control circuits from graph-theoretic specification,” in Proc. IEEE/ACM Int. Conf. Computer Aided Design, Nov. 1990, pp. 184–187. [15] R. K. Brayton, G. D. Hachtel, C. T. McMullen, and A. L. SangiovanniVincentelli, Logic Minimization Algorithms for VLSI Synthesis. Norwell, MA: Kluwer Academic, 1984. [16] F. M. Brown, Boolean Reasoning: The Logic of Boolean Equations. Norwell, MA: Kluwer Academic, 1990. [17] V. I. Varshavsky, Self-Timed Control of Concurrent Processes. Norwell, MA: Kluwer Academic, 1990. [18] K. Lautenbach, “Linear algebraic techniques for place/transition nets,” in Petri Nets: Central Models and their Properties, Advances in Petri Nets 1986, W. Brauer, W. Reisig, and G. Rozenberg, Eds., vol. 254 of Lecture Notes in Computer Science. Berlin, Germany: Springer Verlag, 1987, pp. 142–167. [19] A. Kondratyev, M. Kishinevsky, B. Lin, P. Vanbekbergen, and A. Yakovlev, “Basic gate implementation of speed-independent circuits,” in Proc. ACM/IEEE Design Automation Conf., June 1994, pp. 56–62. [20] M. Kishinevsky, A. Kondratyev, A. Taubin, and V. Varshavsky, “Concurrent hardware. The theory and practice of self-timed design,” Series in Parallel Computing. New York: Wiley, 1994. [21] L. Lavagno and A. Sangiovanni-Vincentelli, Algorithms for Synthesis and Testing of Asynchronous Circuits. Norwell, MA: Kluwer Academic, 1993. [22] A. Yakovlev, L. Lavagno, and A. Sangiovanni-Vincentelli, “A unified signal transition graph model for asynchronous control circuit synthesis,” in Proc. IEEE/ACM Int. Conf. Computer Aided Design, IEEE Computer Society Press, Nov. 1992, pp. 104–111. [23] T. H.-Y. Meng, R. W. Brodersen, and D. G. Messerschmitt, “Automatic synthesis of asynchronous circuits from high-level specifications,” IEEE Trans. Computer-Aided Design, vol. 8, pp. 1185–1205, Nov. 1989. [24] P. A. Beerel, “CAD tools for the synthesis, verification, and testability of robust asynchronous circuits,” Ph.D. dissertation, Stanford University, Stanford, CA, Aug. 1994. [25] S. Burns, “General conditions for the decomposition of state holding elements,” in Proc. Int. Symp. Advanced Research in Asynchronous Circuits and Systems, Aizu, Japan, Mar. 1996, pp. 48–57. [26] J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, E. Pastor, and A. Yakovlev, “Decomposition and technology mapping of speedindependent circuits using Boolean relations,” in Proc. IEEE/ACM Int. Conf. Computer Aided Design, Nov. 1997, pp. 220–227. [27] E. Pastor and J. Cortadella, “Polynomial algorithms for the synthesis of hazard-free circuits from signal transition graphs,” in Proc. IEEE/ACM Int. Conf. Computer Aided Design, Santa Clara, USA, IEEE Computer Society Press, Nov. 1993, pp. 250–254. [28] E. Pastor, J. Cortadella, A. Kondratyev, and O. Roig, “Structural methods for the synthesis of speed-independent circuits,” in Proc. Eur. Design Test Conf. (EDAC-ETC.-EuroASIC), Paris, France, Mar. 1996, pp. 340–347. [29] A. Kovalyov and J. Esparza, “A polynomial algorithm to compute the concurrency relation of free-choice signal transition graphs,” in Proc. Int. Workshop Discrete Event Systems, WODES’96, Aug. 1996, pp. 1–6. [30] E. Pastor and J. Cortadella, “An efficient unique state coding algorithm for signal transition graphs,” in Proc. IEEE Int. Conf. Computer Design, Cambridge, MA, Oct. 1993, pp. 174–177. [31] J. Esparza and M. Silva, “A polynomial-time algorithm to decide liveness of bounded free choice nets,” Theoretical Comput. Sci., no. 102, pp. 185–205, Apr. 1992. [32] O. Roig, J. Cortadella, and E. Pastor, “Verification of asynchronous circuits by BDD-based model checking of Petri nets,” in Proc. 16th Int. Conf. Application and Theory of Petri Nets, Torino, June 1995, vol. 935 of Lecture Notes in Computer Science, Springer Verlag, pp. 374–391. [33] F. Mailhot and G. De Micheli, “Technology mapping using Boolean matching,” in Proc. Eur. Conf. Design Automation (EDAC), Glasgow, U.K., Mar. 1990, pp. 180–185. [34] E. Pastor, J. Cortadella, and O. Roig, “A new look at the conditions for the synthesis of speed-independent circuits,” in Proc. 5th Great Lakes Symp. VLSI, Buffalo, NY, May 1995, pp. 230–235. [35] A. Kondratyev, M. Kishinevsky, and A. Yakovlev, “On hazard-free implementation of speed-independent circuits,” in Proc. ASP-DAC’95, Aug. 1995, pp. 241–248. [36] P. A. Beerel and T. H.-Y. Meng, “Logic transformations and observability don’t cares in speed-independent circuits,” in ACM Int. Workshop Timing Issues in the Specification and Synthesis of Digital Systems, Sept. 1993. [37] P. Siegel and G. De Micheli, “Decomposition methods for library binding of speed-independent asynchronous designs,” in Proc. IEEE/ACM Int. Conf. Computer Aided Design, 1994. Enric Pastor received the M.S. and Ph.D. degrees in computer science from the Universitat Polit´ ecnica de Catalunya, Barcelona, Spain, in 1991 and 1996, respectively. He is an Associate Professor in the Department of Computer Architecture of the Universitat Polit´ ecnica de Catalunya. He was a Visiting Scholar at the University of Colorado at Boulder, CO, and the Inter-university Microelectronics Centre (IMEC), Belgium, in 1992 and 1994, respectively. In 1988, he was a Leverhulme Trust Fellow visiting the University of Newcastle upon Tyne, U.K. His research interests include formal methods for the computer-aided design of VLSI systems with special emphasis on synthesis and verification of asynchronous circuits and concurrent systems. Jordi Cortadella (S’87–M’88) received the M.S. and Ph.D. degrees in computer science from the Universitat Polit´ ecnica de Catalunya, Barcelona, Spain, in 1985 and 1987, respectively. He is an Associate Professor in the Department of Software of the Universitat Polit´ ecnica de Catalunya. In 1988, he was a Visiting Scholar at the University of California, Berkeley. His research interests include computer-aided design of VLSI systems with special emphasis on synthesis and verification of asynchronous circuits, concurrent systems, computer arithmetic, and parallel architectures. He has coauthored more than 80 research papers in technical journals and conferences. He has served on the technical committees of several international conferences in the field of design automation and concurrent systems. Alex Kondratyev (M’97), for a photograph and biography, see p. 771 of the September 1998 issue of this TRANSACTIONS. Oriol Roig received the engineer in computer science degree in 1991 and the Ph.D. degree in computer science in 1997, both from the Universitat Polit´ ecnica de Catalunya, Barcelona, Spain. He was an Assistant Professor at the Universitat Polit´ ecnica de Catalunya until May 1998, when he joined the Methodology group at National Semiconductor, Santa Clara, CA. His research interests include asynchronous and formal hardware verification.