Complete state encoding based on the theory of regions

Complete state encoding based on the theory of regions Jordi Cortadella* Michael Kishinevskyt Alex Kondratyev The University of Aizu Catalunya, 08071 AizuWakamat su, Aizu-Wakamatsu, Barcelona, Spain 965-80 Japan 965-80 Japan Universitat Polithcnica de The University of Aizu Lucian0 Lavagnoj Alex Yakovlevs Politecnico di Torino 10129 Torino, Italy University of Newcastle upon Tyne NE1 7RU England Abstract Synthesis of asynchronous circuits from Signal Transition Graphs involves solving example of such problems is that of Complete State , which happens when a pair of diflerent has the same binary encoding. A siandard way to approach state coding conflicts is to add new state signals into the original specification in such a way that the original behaviour remains intact. Existing methods have not yet been able to provide such theoretical foundation for event insertion, that could yield eficient practical results when applied to large models. This paper aims at presenting such a general framework, which is based on two fundamental concepts. One is a region of states in an abstract labelled SG (called a Transition System . Regions correspond to places in the associated STd! The second concept is a speed-independence preserving set, which is strongly related to the implementability of the model in logic. Regions and their intersections offer “nice” structural properties that make them eficient “construction blocks” for event insertion. The application of our theory, through the software tool petrify, to state graphs of large size has proved to be successful. 1 Introduction The problem of Complete State Coding (CSC) is a fundamental problem in synthesis of asynchronous control circuits from Signal Transition Graphs (STGs) and State Graphs (SGs [2]. This problem arises when a pair of semantically different states in an SG has the same binary encoding. Such states are said to be in CSC conflict. To resolve CSC conflicts, the synthesis *This work has been partly supported by the Ministry of Education of Spain (CICYT TIC 95-0419). tThis work has been partly supported by EPSRC grant GR/ J78334. tThis work has been partly supported by the U.K. SERC GR/J72486 and by MURST research project “VLSI architectures”. §This work has been partly supported by the U.K. SERC GR/ J52327. procedure must insert one or more new signals into the STG (or SG) specification. The value of these new signals have to be different in all pairs of states involved in a CSC conflict. State signal insertion must usually satisfy a set of important requirements: preserving equivalence of the specifications and implementability of the new and the original non-input signals without hazards (speed-independence preservation). The former requirement refers to the language generated by the STG. The latter implies that the implementability conditions (determinism, commutativity, persistency, deadlock-freedom and consistency) must be preserved in the transformed specification. Related Work. A number of methods for solving the CSC problem are known to date [6, 8, 9, 10, 13, 14, 15, 18, 22, 23, 24, 26, 27, 301. Reported experimental results and our own experience with the available tools for solving CSC ensured the authors of this paper that none of the published methods appears to be successful when applied to general SGs or STGs with more than a few thousand states. Methods from [13, 15, 18, 22, 24, 271 work at the STG level without doing state traversal. They allow to avoid state explosion and therefore can process large specifications if some additional constraints on an STG are given. Such constraints (no choice is allowed, or exactly one rising and falling transition €or each signal is allowed, etc.) severely limit the design space and do not allow to get a solution for many practical specifications. [14] solves CSC problem by mapping an initial SG into a flow table synthesis problem and then using classical flow table minimization and state assignment methods. This method is restricted with live and safe free-choice STGs and cannot process large SGs due to limitations of classical state assignment methods. In [23, 261 a very general framework for state assignment is presented. The CSC problem is formulated as state variable assignment on the state graph. The correctness conditions for such assignment are formulated as a set of Boolean constraints. The solution can be found using a Boolean satisfiability solver. Unfortunately, this approach allows to handle only relatively small specifications (hundreds of states) because 0-8186-7298-6/96 $5.00 0 1996 IEEE 36 the computational complexity of this method is double exponential from the number of signals in the SG. Although [6] presented a method to improve the resolution of the method based on a preliminary decomposition of the satisfiability problem, decomposition may produce sub-optimal solutions due to the loss of information incurred during the partitioning process. Moreover, the net contraction procedure used to decompose the problem has never been formally defined for non-free-choice STGs. In [8, 9, IO] another method based on state signals insertion at the SG level was given. At first the excitation regions are distinguished in the SG. These are sets of states, which correspond to transitions of STG. Then the graph of CSC-conflicts between excitation regions is constructed and colored with binary encoded colors. Each bit of this code corresponds to a new state signal. After that new state signals are inserted into the SG using excitation regions of the original or previously inserted signals. The main drawback of this approach was its limitation to STGs without choices. The method described in detail in [29, 301 is probably the most efficient and general published so far. It is based on partitioning of the state space into blocks which contain no internal CSC-conflicts. Similar to [9] a coloring procedure is used to find the optimal number of state signals to resolve all the CSC-conflicts between blocks of partitioning. Each of these state signals can be inserted using as excitation region the sets of states that immediately follow excitation regions (switching regions). Contribution of this paper. This paper provides a general theoretical framework for insertion-based resolution of coding conflicts. The transformations described here are applied to abstract SGs, called Transition Systems (TSs and to binary encoded SGs. This of conflicts between states to be resolved, therefore its application to CSC conflicts is only a special case. Another application of the method may be, e.g., solving Monotonous Cover conflicts [12], for technology mapping of asynchronous circuits in the basis of simple gates (AND, OR, NAND, NOR). It is essential that the theory presented in this paper is based on the concept of regions in a TS. It renders an efficient framework for such transformations due to the two following major reasons. Firstly, regions are subsets of states which have a uniform “crossing” (exit-entry) relationship with events in a TS (see Section 3). They can be easily manipulated in intersections and unions, thus providing a good level of granularity in sectioning the TS (for example the excitation and switching regions are obtained as intersection of preand post-regions for the same transition). Secondly, regions in a TS directly correspond to places in an STG with a reachability graph isomorphic to the TS. This allows reconstructing an STG for the TS with all CSC conflicts resolved - an option much more suitable for the designer than viewing the TS. The concept of regions was firstly presented in [17] and further applied to efficient generation of Petri Nets framework is aime d at being independent of the sort and Signal Transition Graphs from state-based models [4]. The practical implementation of our method, which is only briefly outlined in this paper (those details require a separate presentation), uses symbolic BDD representation of the main objects in the insertion procedure. It has enabled us to solve CSC problem for state graphs with hundreds of thousands of states while the quality of the solutions obtained for smaller state graphs has been quite comparable with other known methods. Our method differs from previous work as follows: 0 Our technique for state signal insertion is more general and allows to explore more solutions than that of [29] and [30], since our method uses regions, their intersections and unions of intersections for insertion. On the other hand, [29] and [30] used excitation regions and switching regions, which are just particular cases of region intersections. Even though the authors of those papers admitted that intersections and unions of intersections of excitation and switching regions “could” be used for insertion, they claimed that “this does not seem necessary in practice”, and did not provide any method for reducing the complexity of the resulting huge search space. The notion of speed-independence preserving set (SIP-set) by which the insertion of state signals can be. done without violation of speedindependence properties is generalized in comparison to [26], as will be shown in detail when discussing Theorem 4.1. e Our method is proven to be complete for a fairly general class of SGs. An additional advantage of the theory presented in this paper is back-annotation at the STG level. The result of CSC resolution is shown to the user as a modified STG, so that the impact of state signal insertion on, e.g., the concurrency of the specification, can be more easily analyzed. From the practical side we observed that although the tool assassin [28] which implements methods from [24, 26, 301 often allows better solutions than other previously known tools, it has difficulties in handling large specifications. For example, a master-read STG with 8932 states ran for more than 24 hours of CPU time at SPARC-10 machine without having solved CSC. Our tool petrify solved this example in 15 min of CPU time. We also solved examples with 10l1 states using a few hours of CPU time. It is worth to mention that on the basis of the region approach petrify succeeded in handling examples that were traditionally difficult for CSC solution by any other tool (see Section 8 for more details). The paper is further organized as follows. Section 2 introduces both state-based and event-based models. Section 3 presents the basics of the theory of regions. Section 4 is dedicated to property-preserving event insertion, which uses the notion of speed-independencepreserving sets (SIP-sets) of states. Section 5 discusses 37 the issue of selection of SIP-sets, based on regions. Section 6 applies the event insertion technique to binary encoded TSs. Section 7 characterizes the set of STGs for which CSC can be solved using the proposed method. Section 8 outlines some experimental results. Finally, Section 9 draws conclusions. 2 State and Event models Transition systems. A transition system (TS) might be viewed as an abstract state graph and is formally defined as a quadruple [17] A = (S,E,T,si,,), where S is a finite non-empty set of states, E is a set of events, T c S x E x S is a transition relation, and Sin is an initial state. The elements of T are called the transitions of TS and will be often denoted by s 5 s’ instead of (s, e, s’). The reachability relation between states is the transitive closure of the transition relation T. A feasible sequence is a (possibly empty) sequence of transitions U between states s and SI (denoted by s 5 s’ or simply by s si.) A feasible trace is obtained from a feasible sequence by removing states. If s1 3 s2, s2 4 s3, s3 3 s4 is a feasible sequence, then el, e2, e3 is the corresponding feasible trace. We also write s 5, 5 s‘, and s 5, 4 st if s -5 s’ or s -41, SI, correspondingly. Note that each state is reachable from itself. A state of a TS is called a deadlock if there is no event e E E such that s $. Furthermore, a TS must satisfy the following four basic axioms: No self-loops, No multiple arcs between a pair of states, Every event has an occurrence, Every state is reachable from the initial state. state = cr,b,c,d> (a) @) (e) Figure 1: An example of Transition System (a), the corresponding SG (b), and STG (c) A TS is called deterministic if for each state s and each label a there can be at most one state s’ such that s 5 SI. Otherwise, a TS is called nondeterministic. In the following we are interested only in deterministic TSs. An example of a deterministic TS is shown in Figure 1,a. State Graph. For the purpose of logic synthesis TSs must be binary encoded. A state graph, SG, is a binary encoded TS. A SG is given by (A,X, As, AE), where signals, and XO is the set of output signals1, such that Each state s E S in the SG is labelled with a binary vector (s(l), .(a), . . . , s(n)) according to the signals X = (21, z2,. . . ,x,} of the system. The labeling is given by a state assignment function AS : S x X cs {0,1}. For a given state s E S, s(i denotes the i-th xi EX. Each event e E E in the SG is labelled with a signal transition. The labeling is given by an event assignment function AE : E H X x {+, -}. Each signal transition can be represented as za+ or zafor the rising (0 .--i 1) or falling (1 ---$ 0) transition of signal ti. zi* is used to depict either a “2i+” transition or a “ii-” transition. Further, if no confusion arises, we will denote different signal names by different letters a, b, . . . instead of zl, 22,. . . Also, (s, zi*, s’) E T stands for (s, e, s’) E T A AE(e) = $a*. An SG has a consistent state assignment (we call such an SG consistent) if the following conditions for assignment functions are met: let (s, e, s’) E T then (1) if AE(e) = zi+, then s(i) = 0 and s’(i) = 1; (2) if.AE(e) = zi-, then s(i) = 1 and s‘(i) = 0; (3) in all other cases s(i) = s’(i). Consistent state assignment is a necessary condition for deriving logic functions for signals encoding a SG [2]. Figure 1,b shows a consistent SG which is obtained by binary encoding of the TS from Figure 1,a. After binary encoding, for example, event c is mapped into signal transition band state sl is mapped into binary code < a, b, c, d >= 0010. is a transition system, X = XI U inary signals, XI is the set of input xInxo =O. component of s corresponding to t h e value of signal Complete State Coding. An unambiguous state assignment is required for deriving logic for encoding binary signals. Logic must be derived only for output signals and therefore the unambiguous state assignment must concern only output signals. This requirement is called Complete State Coding (CSC, [2]): A SG is said to satisfy the Complete State Codang requirement if for any two states sl and s2 which are assigned the same binary vectors the sets of enabled output signals are identical. Let a and b be output and c and d be input signals for the SG in Figure 1,b. States SO and s2 have the same binary code 0110. Output signal b is enabled in nal signals of the modeled circuit. ’The output signals include both external output and inter38 sl and is not enabled in s2, therefore CSC is violated and we say that states SO and 92 are in CSC conflict. Although states s5 and s7 are also assigned the same binary code 1111, they are not in CSC conflict, since no output signals are enabled in s5 and s7. Petri Nets and Signal Transition Graphs. A Petri Net is often a more compact model to represent systems with concurrency than a TS. A Petri Net [20] is a quadruple N = (P, T, F, mo), where P is a finite set of places, T is a finite set of transitions, F C (P x T) U T x P) is the flow relation, is enabled at marking ml if all its input places are marked. An enabled transition t may fire, producing a new marking m2 with one less token in each input place and one more token-in each output place (ml 4 m2). The sets of input and output places of transition t are denoted by ot and to. The Reachability Graph (RG) of a PN is a graph with: a vertex for each reachable marking of the PN and 0 an arc (ml, mz) if and only if ml + m2 in some A net is called safe if no more than one token can appear in a place. Safe nets are used in many applications, since they have simple verification algorithms [5] and simple semantics. A labeled PN is a PN with a labeling function X : T -+ A which puts into correspondence every transition of the net with a symbol (called label) from the alphabet A. A Signal Transition Graph (STG) is a PN whose transitions are labelled with signal transitions (a+, a-, ...). Places with one input and one output transition are called implicit places and are depicted as an arc connecting these two transitions. An STG expressing the same behavior as the SG from Figure 1,b is shown in Figure 1,c. 3 In this section we will briefly review the theory of regions and will show how this theory allows to perform transformations between TSs and PNs (hence, between SGs and STGs). and mo is the initial mar k ing. A transition t E T t firing sequence of the PN. Basics of the theory of regions Regions. Regions are sets of states which correspond to places in Petri Nets. Let S1 be a subset of the states of a TS, SI & S. Ifs S1 and s' E SI, then we say that transition s -% s' enters SI. Ifs E S1 and s' SI, then transition s 5 s' exits SI. Otherwise, transition s 5 s' does not cross 5'1. In particular, if s E SI and s' E SI, then the transition is said to be internal to SI, and if s # SI and s' $! SI, then the transition is external to SI. A subset of states, r, is a region if for each event e exactly one of the following conditions holds: all transitions labelled with e (1) exit r, (2) enter r, or (3) do not cross r. Let us consider the TS shown in Figure 1,a. The set of states r1 = { s5, se, sg} is a region, since all transitions labeled with a and with d exit rl, and all transitions labeled with b and with g enter r1. On the other hand, {sg,sg} is not a region since transition sg 5 SO exits this set, while another transition also labeled with a sg 5 s4, does not. Let r and r' be regions of a TS. A region r' is said to be a subregion of r iff r' C r. A region r' is a minimal region iff r' is not a subregion of any other region of the TS. A region r is a pre-region of event e if there is a transition labeled with e which exits r. A region r is a post-region of event e if there is a transition labeled with e which enters r. The set of all pre-regions and post-regions of e is denoted with 'e and eo respectively. By definition it follows that if r E Oe, then all transitions labeled with e exit r. Similarly, if r E eo, then all transitions labeled with e enter r. There are two pre-regions for event a in Figure 1: r1 = {S~,SS,S~} and r2 = {sg,s7,sg}. Both of them a!e minimal regions, since no subset of r1 or r2 is a region. The following propositions state a few important properties of regions [l, 4, 171. Property 3.1 1. If r and r' are two different regions such that rl is a subregion of r, then T - r' is a region. 2. A set of states r is a region if and only if its coset P = S-r is a region, where S is Q set of all states of the TS. 3. Every region can be represented as a union of disjoint minimal regions. Excitation regions. While regions in a TS are related to places in the corresponding PN, an excitation region 191 for event a is a maximal set of states in which transition a is enabled. Therefore, excitation regions are related to transitions of the PN. A set of states S1 is called a generalized excitation region an excitation region) for event a, denoted by GER(a\ (by ERj(a)), if it is a maximal (a maximal connected) set of states such that for every state s E SI there is a transition s %. The GER for a is the union of all ERs for a. In the TS from Figure 1,a there are two excitation regions for event a: ER1 a) = {sg} and . The corresponding G L R for event a Deriving Petri Nets from Transition Systems. The procedure to synthesize a PN from an elementary TS is as follows: For each event a a transition labeled with a is generated in the PN; 0 For each minimal region ri a place pi is generated; Place pi contains a token in the initial marking mo iff sin E rj; 39 The flow relation is as follows: a E pp iff ri is a pre-region of a and a E bpi iff rj is a post-region of a. This procedure allows to obtain a safe PN with a RG isomorphic to the initial TS or to its minimized version if the initial TS is elementary [17]. As shown in [4] elementarity for minimal TS can be defined by the following two conditions. b Excitation closure. For each event a: n,., oa r = GER(a); b Event effectiveness. FQr each event a: GER(a) # 8; As shown in Figure 1, region r1 is mapped into place TI of the STG. If a TS is not elementary, then it is always possible to transform it to an elementary one by label splitting (one label a which causes violations of elementarity is substituted in the TS by a few independent labels al, a2, . . .) or by inserting dummy transitions. Therefore, for any TS an equivalent safe PN can be synthesized. 4 Constrained transformations of TSs In this section we describe constrained transformations of TSs which preserve equivalence and other important properties. In particular, we formalize the notion of behavioral equivalence for TSs, and we define speed-independence. Speed-Independent Transition Systems. A design is speed-independent if its behavior does not depend on the speed of its components (gates). As shown in [7], two properties ensure that a deterministic TS allows for a speed-independent implementation: persistency and commutativity. The persistency property states that no event can be disabled by any other event. The commutativity property guarantees that the same state of the TS is reached under any order of enabled event firing. Definition 4.1 (Event persistency) Let A = (S, E,T) be a transition system. An event a E E as said to be persistent in r C S iff: Vsl E r : [sl 5 A (sl A s2) ET] =j s2 -% An event a E E 2s saad to be persistent if a as persistent $12 S. Definition 4.2 (Commutativity) A transition system A is called commutative if for any traces ab and ba that are feasible from some state SI E S both truces lead to the same state, i.e., if sl -% s2, s2 -+ s4 and sl + s3, $3 % s5 then s4 = s5. b b Trace equivalence. The set of feasible traces of a TS A is called the language accepted by A and is denoted as L(A). If p is a feasible trace for A, then its projection on a subset of events E1 C E, denoted as p J. El, is a sequence of events p‘ obtained from p by deleting all events from E - El. If L(A) is the language accepted by A, then its projection L(A) 1 El is the set of sequences {p 1 El : p E L(A)}. Let A’ = (S‘, E‘, TI) and A = (S, E,T) be two TSs such that E c E’. Then, TSs A and A’ are trace equivalent if L(A’) 1 E = L(A). Additionally to trace equivalence, the following properties must be preserved after transforming a TS: persistency, commutativity, determinism, and deadlock freedom. The first three properties guarantee that the new TS allows for a speed-independent implementation. The latter property guarantees that liveness of the initial TS is preserved. It is defined as follows: if state s’ is a deadlock in A’ and is reachable from the initial state si,, by a feasible trace p’, then state s of the original TS reachable from sin by a feasible trace p = p’ j. E is a deadlock in A. Event insertion. The basic transformation is the insertion of a single event into a TS. There can be different schemes of event insertion that preserve trace equivalence [3]. In this paper we will rely on a simple one which consists of two steps and is similar to [9, 26, 301 : Choosing in the original TS a set of states r in which the new event x will be enabled. r corresponds to a generalized excitation region of event x in the new TS and therefore is denoted as ER(x) in Figure 2. r until event x fires. 0 Delaying all transitions that exit the set of states Definition 4.3 (Event insertion) Let A = (S, E,T) be a transition system and x 4 E be a new event. Assume that r C S is an arbitra y subset of states. Let r‘, r‘nS = 0, be a set of new states such that for each s E r there is one state s’ E r’ and vace versa. The insertion of x in A by r produces another transition system A’ = (S‘, E’, TI) defined as follows: S’ = S U r’ E‘ = EU {x} T’ = TU {(s 5 s’)Is E r A s’ E r’}U {(sl’ -% s2’)(sl, s2 E T A (sl 5 s2) E T}U {(SI’ 5 s2)lsl E r A s2 {(SI Z s2)lsl E r A s2 6 r} r A (SI 5 s2) E T}- By Definition 4.3 transforming A to A’ via adding the new event x by a set of states r leads to splittin all states s E r in S into two states s and s‘ in SI. AB other states s 6 r are in correspondence with only one state in SI. Figure 2 illustrates how event insertion is performed. 40 S-ER(x) S-ER(x) Figure 2: Insertion of event x from ER(x) Speed-independence preserving sets. It is easy to show that the insertion of event 2 by Definition 4.3 always preserves trace equivalence, determinism and deadlock-freedom [3]. Persistency and commutativity, on the other hand, are not automatically preserved, and need a more careful analysis. Definition 4.4 (SIP-set) Let A = (S, E,T) be a transition system, x e E be a new event and r E S. Let A‘ = (S’, E’,T’) be a transition system obtained after inserting x by r. r is said to be a speedindependence preserving set (SIP-set) iff: 1. Va E E : a is persistent in A =$- a is persistent in A’ 2. A is commutative Ifr satisfies only condition 1 then r is a persistency preserving set. The following theorem determines two conditions for preserving persistency and commutativity. A’ is commutative A’: s4 Y s4 s3’ s2’ bQ s4 (b) Figure 3: Set of states r is not persistency preserving. Theorem 4.1 Let A = (S, E,”) be a TS and r C S a subset of states. r is a persistency-preserving set iff [(sl 5 s3),(s2 5 s4),(sl 5 $2) E T A s2 E Let A = (S, E, T) be a commutative transition system and r c S be a persistency preserving set. Then r is a SIP-set iff: r,s4#r] a slEr A s39r (1) b b sl s2, s2 --$ $4, sl + s3, s3 5 s4 E TA This theorem refines conditions for speed-independence from [23]. It allows to handle correctly the so called asymmetric “fake” conflicts between signals (kl]). Consider, for example, Figure 3.(a), where t ere is no arc between s3 and s4. On the other hand, SIP conditions were defined in [23] only with respect to complete diamonds of states. Hence, the conditions stated in [23] are not sufficient to find the violation of persistency in cases like that of Figure 3,a. Figure 3 shows two possible cases of violation of the persistency preserving condition (1) from Theorem 4.1. In both cases event b becomes non-persistent. Note that event x is persistent by construction in the TS obtained after the insertion. Hence, if a persistency preserving set is used for signal insertion, then no new non-persistencies can arise. (sl, s2 E r A s3 $2 r) s4 # r (2) s4’ Figure 4: Commutativity violation after signal insertion Figure 4 shows a violation of commutativity when a set of states r does not meet condition (2) of Theorem 4.1. Figure 5 shows allowable correct intersections of a SIP-set with all state diamonds in a SG. 5 Selecting SIP-sets This section presents a few basic properties which allow us to formulate improved strategies for selection of SIP-sets. In 123, 26 SIP-sets are selected by solvthe search space for SIP-sets is problematic since in the reduction to the satisfiability problem each state in SG is considered separately (it is encoded by two binary signals) that quickly leads to unmanageable complexity when solving the satisfiability instance. In [8, 9, 101 SIP-sets are constructed from excitation regions of the original signals and previously introduced state signals. [30] generalized this method in such way that both ERs and switching regions (SRS) are used for SIP-sets. In this paper we further generalize this method: SIP-sets are constructed as regions, their intersections and union of intersections. We will show below that re ions ensure to automatically find valid SIP-sets, rat%er than checking for SIP a posteriori, which is considerably less efficient. Note that Eh and SRs are particular cases of region intersections. Therefore, our method allows to explore a larger search space for SIP-sets and to find more efficient solutions. ing a satisfiability pro lb lem. Efficiently constraining 41 sl 2 ySia AA2 s3 s4 s4 Figure 5: SIP-sets for a state diamond Property 5.1 If r is a region in a commutative elementary transition system, then r is a SIP-set. The proof of this property is trivial. At the PN level this property corresponds to a following structural transformation: place r is substituted by two places r and r’ with a new intermediate transition labelled with x. Place r has only one output transition, x, and all transitions which belong to re in the initial PN belong to r’o in the new PN. Obviously, such transformations cannot violate persistency or commutativity for any event. Property 5.2 If r is an excitation region of event c in a commutative transition system A and c is persistent in r, then r is a SIP-set. Intuitively, this property can be stated as follows: delaying a persistent event cannot create violations of persistency or commutativity. At the PN level this means that substituting a persistent transition by a sequential composition of two transitions preserves persistency and commutativity. At the circuit level this property corresponds to a well-known fact: inserting delays at the gate outputs before a wire fork does not violate semi-modularity of the circuit [16]. Most of the previous methods for CSC used variations of property 5.2 [2, 9, 14, 23, 301. Definition 5.1 (Exit and input border) Let A = (S, E,T) be a transition system. Given a subset of states r C S, the exit border of r (denoted as EB(r)) and the input border of r (denoted as IB(r)) are defined as follows: EB(r) = {s E r13a E E, s’ E S : s 3 s’ E T A s‘ # r) IB(r) = (s E r[3a E E, s’ E S : s’ 5 s E T A s’ g‘ r} Exit borders of regions and intersection of preregions of the same event can also be safely used as SIP-sets under the following conditions. Property 5.3 Let A = (S, E, T) be a commutative elementary transition system and let r be Q region in A. If all the exit events of r are persistent then EB(r) as a SIP-set. Proof: If Condition 1 for a SIP-set is violated, then s2 E EB(r) and s4 6 EB(r). Hence, there exists event c such that s2 5 s5, s5 $Z r. Clearly c is an exit event for r and from the properties of a region any state in which c is enabled belongs to r. If c # b then from s4 EB(r) follows that event c, which is enabled in s2, becomes disabled in s4. This contradicts the assumption that all exit events of r are persistent. If c = b then sl-belongs to EB(r) contradiction with Figure 3,a) and 93 must be out of r I contradiction with Figure 3,b). 2. Violations of Condition 2 (Figure 4). By the same consideration if c # b then c becomes disabled in s3. If c = b then s4 cannot be in EB(r). 0 A set of states S is called forward connected if for any pair of states s1 , s2 E S there is a state s3 E S (s3 may coincide with SI or with s2) such that si 273, s2 2 s3 and all states of U and a1 belong to S. Property 5.4 Let A = (S, E,T) be a commutative elementary transition system and let rl, r2 be preregions of the same event. If r1 n r2 is forward connected and all exit events of rlnrz are persistent, then r1 n r2 4s a SIP-set. Proof: Assume that A = (S, E, T) is a commutative elementary transition system. Assume also that r1 , r2 are pre-regions of the same event b E E, r1 n 7-2 is forward connected, and all exit events of r1 n 9-2 are persistent. Let us prove that r1 n r2 is a SIP set, i.e., rl n r2 is persistency-preserving and commutativitypreserving. Assume that A’ is the TS obtained after inserting a new event x by r1 n r2. We need to prove that persistency and commutativity are preserved in A’. Persistency preservation. (1) A new event x and all events from E which do not exit r1 n r2 are persistent in A‘ by construction. (2) Consider event b. Let us refer to condition (1) from Theorem 4.1 and Figure 3. Since rl, r2 E ob, all transitions labelled with b must exit both r1 and r2. Hence, sl -+ s3 exits both r1 and rz and therefore, 1. Violations of Condition 1 (Figure 3). b b sl 4 s3 exits r1 n r2. Condition sl E r1 n r2 A s3 6 r1 n r2 is satisfied and persistency holds by Theorem 4.1. 42 (3) Consider event b’ other than b such that b’ exits r1nr2 but rl or r2 are not pre-regions for b’. Transition 92 5 s4 from condition (1) of Theorem 4.1 exits r1 n r2. Hence, s2 --+ s4 exits either r1 or r2. Let us assume, for example, that s2 + s4 exits r1. Then transition sl -+ s3 also exits r1. Let s2 E GER(b). Since b is persistent and s2 5 94, state s4 E GER(b) and s2 -% s4 is internal to GER(b). In an elementary TS the intersection of pre-regions for the same event b gives the excitation region for b. Hence, s2 --+ s4 is internal to r1 and we have reached a contradiction. Let s2 E (rlnrZ)-GER(b). Since rlnr2 is forward connected three cases are possible: (2) 3s’ E GER(b) : s’ 5 s2, and (3) 3s’ E GER(b), SI’ E (r1 n ra) - GER(b) : s2 b’ b’ b’ b’ (1) 3s‘ E GER(b) : ~2 Z. s‘, A 01 I’ +s. Let us consider the first case. Event b’ is persistent and since b’ exits r1, the following condition holds: 6’ U. Therefore, there is a state s5 such that s‘ ---t s5. Since s’ E GER(b) and b is persistent the following holds: s5 +. Therefore, s5 E GER(b) and s’ + s5 is internal for GER(b) transition. Hence, s’ + s5 is internal to r1 and we have reached a contradiction with the assumption that b’ exits r1. Let us consider the second case. Since b is persistent, r1 n 1-2 is forward connected and both r1 and ~2 are pre-regions for b, then event b $ U. Therefore, state s2 E GER(b) and both b and b’ are enabled in 62. Since b is persistent we may conclude that transition s2 + is internal for GER(b) and hence is also internal for 7-1. We again have reached a contradiction. Let us consider the third case. Since b is persistent, r1 n 1-2 is forward connected and both r1 and r2 are pre-re ions for 6, event b is enabled in s” which implies third case to the first case, which has been already considered. Commutativity preservation. Let us refer to condition (2) from Theorem 4.1 and Figure 4. Given a diamond sl 5 s2, s2 -+ s4, 61 s3, s3 s4, the commutativity property may be violated only in one case: if state s3 $ rlnr2 and states sl, 92, s4 E rlnr2. In such case transition sl A s3 exits n r2 and therefore must exit r1 or r2. Assume for example that sl -+ s3 exits r1. On the other hand, transition s2 + s4 is internal for rl n r2 and hence does not exit r1. We have reached a contradiction with the definition of a region. 0 A significant consequence of these properties is that the good candidates for insertion can be built b’ b b’ b’ b’ that s $1 E GER(b). Therefore, we have reduced the b b b b on the basis of regions and their intersections, since they guarantee to preserve equivalence and speedindependence. One may also conclude that SIP-sets for event insertion can be built very efficiently from regions rather than states. 6 Transformations of State Graphs The binary encoding of a TS to obtain an SG implies additional constraints for inserting new events: each inserted event has to be interpreted as a signal transition and therefore consistency of state assignment must be preserved. Any event insertion scheme which preserves trace equivalence (like those in Definition 4.3) also preserves consistency for the original signals. Special care must be taken to ensure consistency of the new signals (that are usually called state signals). A specific class of SGs transformations can be defined as follows: 1. Insertion is made by signals not by events. Therefore, instead of inserting a single event two signal transitions of a new signal are inserted at each step: z+ and z-. Two sets of states for insertion, GER(z+) and GER(z-), are defined simultaneously such that GER(z+) n GER(z-) = 0. 2. Similar to TSs transformations, both sets for insertion, GER(z+) and GER(z-), must be SIPsets. In addition, consistency of state assignment for signal x is required. Given an SG with a set of binary states S, a partition for the insertion of signal x, called I-partition, is a partition of S into four blocks ([25]): So, 6, S+ and S-. So(S1) defines the states in which x will have the stable value 0 (1). S+(S-) defines GER(z+) Let A be a consistent SG and let I = {So, S1, S+ S-} be an I-partition of A. SG A‘ obtained by inserting signal x by partition I is consistent iff the only allowed arcs crossing boundaries of the partition blocks are the following: So +. S+ --+ S1 + S- --i So, S+ + Sand S- -+ S+, S+ -+ So and S- --.* S1. Arcs like those shown in Figure 6 are forbidden. The proof of this property trivially follows from the rules of insertion for events z+ and z- (see Definition (GER( z-)). 4.3). SO I h J, S’ Figure 6: Illegal transitions in an I-partition An I-partition can be found in two steps: 43 0 Find a bipartition {b, b}, (6 = S - b) of S. The value of signal 2 is constant inside blocks b and 6. 0 Choose GER(x+) and GER(x-) at the boundaries of blocks b and 5 respectively. The boundaries might be defined in two ways: as exit borders or as input borders. Figure 7,a shows insertion by exit borders: given a bipartition (b,&}, GER(z+) = EB(b) and GER(x-) = EB(5) (or vice versa). Figure 7,b illustrates insertion by input borders. In this case GER(x+) = IB(b) and GER(x-) = IB(6) (or vice versa). \ / x=l / x= 1 S-r b) Figure 7: Signal insertion by exit (a) and input (b) borders In general, using exit and input borders as insertion sets for new signal transitions does not always guarantee the consistency for the new signal. It may be necessary to enlarge the exit border EB(b) with those states of the block b which are directly reachable from EB(b). Similarly, for input border IB(b) an enlargement is required with those states of b from which IB(b can be entered. Such enlargement is not Definition 6.1 Let {b,T} be a bipartition of a SG states. 1. The exzt border EB(b) is called well-formed iffVs EB(b) : [t/s 5 s’ : s‘ E 6 U EB(b)] (similarly for necessary i 2 a border is well-formed. input border IB(b) is called well-formed iff Vs E IB(b) : [Vs’ 1 s : s’ E TU IB(b)] (similarly for IB(~)) . Let us refer to Figure 6. If well-formed exit borders are chosen for inserting new signal transitions, then the I-partition is defined as follows: So = b - EB(b), S+ = EB(b), S1 = bEl?($), S- = EB 6 . Since a transition can exit b only through the EB[b), no arcs So -+ 6 and So Sin Figure 6 are possible. Due to the well-formedness of EB(b) it is not possible to return from EB(b) to b-EB(b), hence arcs S+ 3 So are not possible either. A similar reasoning holds for EB(b), hence none of the illegal transitions from Figure 6 can occur. Property 6.1 Let A be a consistent SG with a set of states S partitioned into {b,&}. The SG A‘ obtained by inserting signal x by exit (input) borders of {b,b) is consistent iff these borders are well-formed. If the borders of a given partition {b,6} of S are not well-formed, we can still use it by considering larger sets of states that guarantee consistency. Namely, given {b,T;), we can define minimal wellformed extended EB and IB (denoted MWFEEB(b) and MWFEIB( b)) as minimal well-formed enlargements of exit and input borders respectively. MWFEEB(b) can be calculated as the least fix point of the following recursion: 1. MWFEEB(b) = EB(b) 2. [s E MWFEEB(b) A s’ E b A s -s’] j s’ E MWFEEB(b) A similar recursion can be applied for calculating M W FEEB(z), M W FE I B( b) , and M W F El B(6). Minimal well-formed extended borders hence are minimal sets of states for signal transition insertion which guarantee consistency. 7 Completeness of the method In this section we will show that the method for CSC solution using region-based signal insertion is complete, i.e. it allows to solve all CSC conflicts, for a fairly general class of SGs. A direct synthesis method for speed-independent implementation of STGs without choice has been proposed in [9]. It solves all CSC conflicts by construction. This method can be generalized to any safe STG [3] which is persistent with respect to the transitions of output signals (so called output-persistent STGs). Hence, this direct method can be applied to any SG for which a safe and output-persistent STG can be generated using regions as described in Section 2. Generating such an STG is possible if an SG satisfies the following conditions: (1) it is deterministic, consistent, commutative and persistent by output signals, and (2) it is elementary after splitting all GERs into E%. This result implies that for each SG which meets these conditions, the procedure of signal insertions based on intersection of regions will eventually converge. Let us have a closer look at an I-partition, in order to estimate an upper bound on the number of state signals needed to solve all CSC conflicts. Assume that (b, 6} is a bipartition of a set of states. Assume that an I-partition is constructed from {b, 6} by exit borders, i.e., S+ = MWFEEB(b), S- = MWFEEB(8) and So = b - S+ , S1 = b - 5’- (see Figure 7,a). Clearly, all the states from So and S1 will differ in the new SG obtained after the transformation by the 44