Sequential Flexibility Overview • Computing flexibilities in combinational logic • networks FSM networks – Computing sequential flexibilities – Contrasting combinational and sequential flexibility computations – FSM minimization using register splitting • Examples Minimizing a Node – Computing the Flexibility at a Node Combinational Logic Network Definition. A flexibility at a node is a relation (between the node’s inputs and output) such that any welldefined sub-relation used at the node leads to a network that conforms to the external specification. Definition. The complete flexibility (CF) is the maximum flexibility possible at a node. Computing the CF for a node global step yi X Z R( X , yi , Z ) R( X , yi ) Z [ R( X , yi , Z ) R spec ( X , Z )] Computing CF - local step Yi X Yij yi yi Z M ( X , Yi ) CF (Yi , yi ) X [ M ( X , Yi ) R( X , yi )] CF (Yi , yi ) X [ M ( X , Yi ) Z [ R( X , yi , Z ) R X , Z [M ( X , Yi ) R( X , yi , Z ) R spec spec ( X , Z )]] ( X , Z )] CF yi Yi yi X Z M ( X , Yi ) M ( X , Yi ) Yi yi CF (Yi , yi ) X [ M ( X , Yi ) Z [ R( X , yi , Z ) R X , Z [ M ( X , Yi ) R( X , yi , Z )]R spec spec (X , Z) Note that essentially the same computation applies for multiple-output 1 k nodes, i.e. where yi { yi , , yi } ( X , Z )]] FSM networks • Network of finite state machines (FSMs) i1 FSM Sequential FSM FSM i2 Problem: Compute the Complete FSM FSM FSM FSM o Flexibility of a node Complete Sequential Flexibility CSF is the maximum set of FSM behaviors (represented by a pseudo-non-deterministic FSM), such that implementing any sub-behavior and replacing the sub-network by the new implemented part does not violate the specification of the total network. FSMs and Automata If the distinction between inputs and outputs is taken away (i/o becomes io), then an FSM becomes an automaton. It has the following properties as an automaton – All states are accepting – It is incomplete • can make it complete by adding one nonaccepting state – Its language is • prefix closed • i -progressive 0/0 0 0 0/0 0 0 Automaton FSM 1/1 1 1 1/0 1 0 1/0 1 0 0/0 0 0 FSM networks – computing complete sequential flexibility (CSF) i1 FSM FSM FSM i2 i Specification S (i,o) FSM FSM FSM FSM o spec context v u unknown o Context C (i,v,u,o) Unknown X (u,v) Problem: Given S and C, find the Most General Solution (MGS) of X CS FSM Networks i The most general solution (MGS) of X CS spec context v o u unknown is MGS (C ( S )( i ,v ,u ,o ) )( u ,v ) In general, MGS is deterministic automaton but as an FSM it is non-deterministic (NDFSM) Languages. A Language is set of finite length strings on the symbol set i.e. a subset of * (a b c a c d f g g g) At this point, we don’t care how the language is generated or represented. So initially the comments apply to all kinds of languages A symbol can be made up of a vector of variable values, e.g. 1a3de0 or 010010. These are examples of a single symbol. Languages can be manipulated as follows: • Union L1 L 2 { | L1 or L 2 } Intersection L1 L 2 { | L1 L 2 } Complement L { | L } * Language over cross-product of alphabets • A language over X Y where X and Y are symbol sets consists of finite strings of pairs ( 1 , 1 ), ( 2 , 2 ), , ( k , k ) Such that i X and i Y Projection and Lifting Given a Language L over the alphabet X Y projection is defined as – L X {{ X } | {( X Y )} L } i i i Given a Language L over the alphabet X lifting to the alphabet X Y is defined as L Y {{( X )} | { X } L } i i where - stands for any symbol in Y Classes of Languages A language is prefix closed if , ,[ L L ] * A language over I O is I-progressive if , i I , o O [ L io L ] * Composition of Languages Given disjoint alphabets I,U,O and languages L1 over I U and L2 over U O their synchronous composition is L1 L 2 [( L1 ) O ( L 2 ) I ] I O . Solving a language equation Theorem A: Let A and C be languages over alphabets I U and I O respectively. For the equation, A X C the Most General Solution is X ( AO CU )U O I A U X O Proof: We prove Theorem A. Let (U O)*. Then A C means that ( AO I ) I O C ( AO I CU ) I O AO I CU I ( AO I CU )U O A U X ( I )U O ( AO CU )U O O ( AO CU )U O ( AO CU )U O AC Thus A C is the largest solution of A X C Complete Sequential Flexibility (CSF) • CSF is maximum sub-behavior in MGS which is prefix closed and u-progressive. – For unknown to be an FSM, it must be progressive in its inputs u v CSF Example: Coin Game (NIM) In God We Trust In God We Trust In God We Trust 1. 2. 3. Context describes the state of the game and legal moves. Its input is random moves by first player and its output tells if the game is in a losing state. Specification is a 3-state automaton, playing, won, and lost. Players alternate turns On each turn, player can take 1-n coins from any one pile Player who takes last coin loses Winning strategy: Give your opponent a pile of coins with even number of 1’s in bit columns (except at end) Example: 5 3 6 6=110 5=101 3=011 ____ 222 Example of CSF computation: NDFSM represented as automaton The CSF is a non-deterministic FSM 5 inputs, 5 outputs, 21 states, 34 transitions Inputs p1_0 p1_1 d1_0 d1_1 d1_2 Outputs p2_0 p2_1 d2_0 d2_1 d2_2 In God We Trust In God We Trust In God We Trust Computational Procedure Computing the transition relation of CSF 1. Complement S 2. Raise S to variables of Specification: S (i,o) Context: C (i,v,u,o) (these have been converted into automata) S C ( S )( i ,v ,u ,o ) 3. Compose S with C (C ( S )( i ,v ,u ,o ) ) 4. Hide variables not in X (C ( S )( i ,v ,u ,o ) )( u ,v ) 5. Complement result (C ( S )( i ,v ,u ,o ) )( u ,v ) Finite Automata A finite automaton (FA) is F ( S , , , r , Q ) where S is a set of states, is an input alphabet, ( s, ) : S 2 S is a transition relation, r is the initial state, and Q S is the set of accepting states. An input sequence w ( w1 ...w n ) * leads from r to s’ if there exists a sequence of states, ( r s 0 s1 ... s n s ') such that s i 1 ( s i , wi ) for all i = 0, ... ,n-1. w is in the language of F ( w L ( F ) ) if and only if w leads from r to s ' Q i.e. ( r , w ) Q where ( r , w ) denotes the set of states that can be reached from r under the input sequence w. Theorem: A languages is regular if and only if it is the language of a finite automaton Theorem: The set of all languages for deterministic FA is the same as for non-deterministic FA. (this can be shown by using the so-called subset construction.) Operations on FA. projection ( F X ): convert F over X V into F’ over X by replacing each edge (xv s s’) by the edge (x s s’) lifting (FV ): convert F over X into F’ over X V by replacing each edge (x s s’) by ( x V s s ') where V stands for any v V . Operations on FA. Product Given FAs F1 and F2 both over , the product is F F1 F2 ( S 1 S 2 , , , ( r1 r2 ), Q1 Q 2 ) where ( s1 s 2 , ) 1 ( s1 , ) ( s 2 , ) Complementation If F is deterministic, thenF ( S , , , r , Q S Q ) . If F is non-deterministic, the only known way for complementation is to determinize it first. This is done by the sub-set construction. Composition Synchronous Composition. Given two automata F1 and F2 over alphabets I U and U O their synchronous composition is F1 F2 ( F1 ) O ( F2 ) I i.e. the product of the two automata when they are made to have the same alphabet. Subset Construction Given NFA F ( S , , , r , Q ) we create a DFA F’ with the same language as F: F ' (2 , , ',{ r }, Q ') S S where Q ' { s ' 2 | qQ , q s '} and '( s ', ) { s | sˆs ' , s ( sˆ , )} s’ Theorem: F and F’ have the same language. Proof: q ( r , w ) q '({ r }, w ) Finite State Machines as Automata A FSM is M ( S , I , O , T , r ) where I is the set of input symbols, O the set of output symbols, r the initial state, and T(s,i,s’,o) is the transition relation. A transition (s,i,s’,o) from state s to s’ with output o can happen on input i can if and only if ( s , i , s ', o ) T ( s , i , s ', o ) If ( s , i ) ( s ', o )[( s , i , s ', o ) T ] then M is complete, otherwise partial. It is deterministic if for all (s,i) there is at most one (s’,o) such that ( s , i , s ', o ) F It is pseudo-non-deterministic if for all (s,i,o) there is at most one s’ such that ( s , i , s ', o ) F Converting an FSM to an automaton An FSM M can be converted into an automaton F by the following: F ( S , ( I O ), , r , S ) where ( s , io ) { s ' | ( s , i , s ', o ) T } Note that Q = S, i.e. all states are accepting The resulting automaton is typically not complete, since there are io combinations for which a next state is not defined. We can complete it by augmenting to include a transition to a new non-accepting state DCN. f s f DCN FSMs as Automata The language of an FSM is defined to be the language of the associated automaton A pseudo non-deterministic FSM is one whose automaton is deterministic. The language of an FSM is prefix closed. The language of an FSM is I-progressive Conversion M F is done by grouping i/o on edges to (io) and making all states accepting. Conversion F M can be done only if the language is prefix closed and I-progressive. In this case, delete all non-accepting states (prefix), and change edges from (io) to i/o. Computational Procedure Computing the transition relation of CSF 1. Complement S 2. Raise S to variables of Specification: S (i,o) Context: C (i,v,u,o) (these have been converted into automata) S C ( S )( i ,v ,u ,o ) 3. Compose S with C (C ( S )( i ,v ,u ,o ) ) 4. Hide variables not in X (C ( S )( i ,v ,u ,o ) )( u ,v ) 5. Complement result (C ( S )( i ,v ,u ,o ) )( u ,v ) Comparison with combinational case Sequential CSF (u, v) i ,o (C ( S )( i ,v ,u ,o ) ) ( u ,v ) i spec context u o v unknown Combinational CF (Yi , yi ) X , Z [ M ( X , Yi ) R( X , yi , Z )]R spec (X , Z) X , Z [ M ( X , Yi ) R ( X , yi , Z ) R( X , yi , Z ) X M ( X , Yi ) Yi yi unknown R spec ( X , Z )] Application - splitting FSM blif files u i FSM FSM1 o v FSM2 A run on s298.blif splitting 14 latches into 7 each mvsis 07> source langi.script Extracting STG of spec ... The extracted STG has 218 states and 1078 transitions. Extracting STG of fixed ... The extracted STG has 43 states and 128 transitions. Extracting STG of particular solution ... The extracted STG has 20 states and 400 transitions. Determinizing the spec ... The automaton is deterministic; determinization is not performed. Computing the product ... Product: (43 st, 128 trans) x (219 st, 1297 trans) -> (966 st, 9975 trans) Determinizing the product and making progressive... The automaton is deterministic; determinization is not performed. Checking containment … The solution composed with fixed is contained in the spec. The particular solution is contained in the solution mvsis 13> psa x.aut x.aut: The automaton is incomplete (552 states) and deterministic. mvsis 13> minimize x.aut x-min.aut State minimization: (554 states, 5674 trans) -> (272 states, 2704 trans) X-min.aut but not from splitting s298 (too big to show); instead from splitting s27 The End

Descargar
# Document