Sequential System Synthesis -- Finite State Machine. Outline: Finite State Machine. Definitions FSM Representations State Transition Graph (STG) Flow Table Cube Table State Minimization Completely Specified FSM Incompletely Specified Machine (ISM) State Encoding.

All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.

Share

Transcript

Sequential System Synthesis-- Finite State MachineOutline: Finite State MachineDefinitions FSM Representations State Transition Graph (STG) Flow Table Cube Table State Minimization Completely Specified FSM Incompletely Specified Machine (ISM) State Encoding ENEE 644Definition: Finite State MachineA Finite State Machine (FSM) of Mealy type is a 6 tuple <I,S,,S0,O,> I: input alphabet, a non-empty set of input values; S: a non-empty, finite set of states; : SxI S, a function defines the next state; S0: S, the set of initial/reset states; O: output alphabet; : SxI O, a function defines the output. A finite state machine of Moore type is defined in the same way except that the output function : S O does not depend on the present inputs. ENEE 644Example: Finite State MachineI = {x,y} S = {A,B,C} S0= {A} (A,x) = A, (B,x) = A, (C,x) = C (A,y) = B, (B,y) = C, (C,y) = AO = {0,1} (A,x) = 0, (B,x) = 0, (C,x) = 0 (A,y) = 1, (B,y) = 0, (C,y) = 1ENEE 644FSM Representation: STGIn sum, a STG is a weighted, directed graph where self loops and duplicated edges are allowed. Each node has at most |I| outgoing edges and |I|x|S| incoming edges. Total number of edges is |I|x|S|+|S0|. State Transition Graph: Node state (S) Edge transition ( : SxI S, : SxI O, S0) Direction: from the current state to the next state Label: input/output information for the transition Special edges: edges without source, their ending nodes are initial states ENEE 644x/0Ay/1x/0y/1y/0CBx/0Example: FSM as an STGI = {x,y} S = {A,B,C} S0= {A} (A,x) = A, (A,y) = B, (B,x) = A, (B,y) = C, (C,x) = C, (C,y) = AO = {0,1} (A,x) = 0, (A,y) = 1, (B,x) = 0, (B,y) = 0, (C,x) = 0, (C,y) = 1ENEE 644x/0Ay/1x/0y/1y/0BCxyAB,1x/0BA,0C,0CC,0A,1FSM Representation: Flow TableThe flow table of an FSM <I,S,,S0,O,> is a |S|x|I| table, where the i-th row represents state Si, the j-th column represents input value xj. The entry at (i,j) is a 2 tuple <(Si,xj), (Si,xj)>. The initial states S0 can be specified separately. Example: A,0ENEE 644x/0Ay/1IPSNSOx/0y/1xAA0y/0CBxyAyB1xBA0AA,0B,1x/0yBC0BA,0C,0xCC0CC,0A,1yCA1FSM Representation: Cube TableThe cube table of an FSM <I,S,,S0,O,> is a (|S|x|I|)x4 table, where in each row, the first column represents input value xj, second column is the state Si, third column is the next state (Si,xj), and the last column is the output (Si,xj). The initial states S0 can be specified separately.Example: ENEE 644FSM with Incomplete SpecificationAn FSM <I,S,,S0,O,> is incompletely specified if and/or are incompletely specified functions. (I.e., they are not defined on some combinations of inputs and present states.) Otherwise, it is completely specified. In STG, this means there exist nodes with less than |I| outgoing edges; In flow table, this means there exist undefined entries; In cube table, this means there exist undefined rows. ENEE 644Make Incomplete CompleteIn STG: add a dummy state called trap state. In flow table: leave the entry empty or fill it by <don’t care, don’t care>. In cube table: delete the undefined row or fill the last two columns by don’t cares. y/-x/0x/0AADDx/-y/1y/1y/1y/1x/0x/0?x/-y/0y/0BCBC-/-ENEE 644FSM MinimizationFSMs may contain redundant states, i.e. states whose function can be accomplished by other states. Removing the redundant states decreases the number of states in the FSM, and in general results in a simplification in the final implementation. State minimization is the transformation of a given FSM into an equivalent FSM with no redundant states (I.e. minimal number of states). ENEE 644compatibility relationBinary RelationsGiven two sets A and B, a binary relationR between A and B is a subset of AxB={(x,y)|xA,yB}. We write xR y if (x,y)R . Relation R BxB is reflexive iff xRx for any xB; symmetric iff xR y yR x; anti-symmetric iff xR y, yR x x=y; transitive iff xR y, yR z xR z. A binary relation R BxB is an equivalent relation if it is reflexive, symmetric, and transitive. ENEE 644Partition into Equivalent ClassesA partition of a set of B is a set of subsets BiB, such that BiBi (ij) iBi=B. Given an equivalent relation R BxB, the equivalent class of xB is [x]={yB|xRy}. x,yB, [x]=[y] or [x][y]=; If B1,B2,…,Bn are all the different equivalent classes, then {B1,B2,…,Bn} is a partition of B. An equivalent relation gives a unique partition.ENEE 644Refinement of a PartitionGiven two partitions P1={B11,B21,…,Bm1} and P2={B12,B22,…,Bn2} of a set B, P1 is a refinement of P2 if every subset (block) Bi1Bj2 for some j. Let P1={B11,B21,…,Bm1} and P2={B12,B22,…,Bn2} be two sets of subsets of a set B, the meet of P1 and P2 is defined as the following set: P1•P2={Bi1Bj2|i=1,2,…m,j=1,2,…,n} Theorem: If P1 and P2 are partitions, then P1•P2 is also a partition of the same set B, furthermore, it is a refinement for both P1 and P2. [Proof:]ENEE 644st==?stEquivalent States of an FSMGiven two states s and t in an FSM, and a k-string x=(x0x1…xk-1), suppose zs=(zs0zs1…zsk-1) and zt=(zt0zt1…ztk-1) are the corresponding output strings when states s and t are used as starting state respectively. x is called a length-k distinguishing sequence for states s and t iff zsk-1 ztk-1. xk-1…x1x0zsk-1…zs1zs0xk-1…x1x0ztk-1…zt1zt0ENEE 644Equivalent States of an FSMTwo states s and t are k-equivalent, written as skt, iff there does not exist a distinguishing sequence for s and t of length k or less. Two states are equivalent iff they are |S|-equivalent. Define k={(s,t)| skt}, the set of all pairs of k-equivalent states. k is an equivalent relation, I.e., it is Reflexive: sks Symmetric: skt tks Transitive: rks, skt rkt ENEE 6440/0BD0/01/00/01/11/0AF1/00/01/11/10/0EC0/0Equivalent States of an FSM1={(A,C),(A,E),(C,E),(B,D),(B,F),(D,F), (C,A),(E,A),(E,C),(D,B),(F,B),(F,D), (A,A),…,(F,F)} B11={A,C,E} B21={B,D,F} 2={(A,C),(A,E),(C,E),(B,D), (C,A),(E,A),(E,C),(D,B), (A,A),…,(F,F)} B12={A,C,E} B22={B,D} B32={F} 3={(A,C),(B,D),(C,A),(D,B),(A,A),…,(F,F)} ENEE 644Equivalent States Checking: TheoryTwo states are equivalent iff they are |S|-equivalent. Theorem 1. Let sx and tx be the x-successors of s and t in an FSM, then sk+1t skt and xI, sxktx.Theorem 2. Two states of a given FSM are equivalent iff they are (|S|)-equivalent.ENEE 644State Equivalence Checking: PracticeGoal: determine |S|(S), all pairs of equivalent states in an FSM S. Partition-Refinement procedure: Pk={B1k,B2k,…}: the partition determined by k, the k-equivalent state pairs. (P0=S={B10}) Idea: For each block in Pkpartition it (for all xI) if its x-successors are not in the same block; Refine the partition by taking the meet of these finer partitions; Stop when Pk+1=PkENEE 644PS NS, z x=0 x=1A E, 0 D, 1B D, 0 F, 0C E, 0 B, 1D B, 0 F, 0E C, 0 F, 1F B, 0 C, 00/0BD0/01/00/01/11/0AF1/00/01/11/10/0EC0/0Example: Finding Equivalent States P0={(A,B,C,D,E,F)} (1-block)P1={(A,C,E),(B,D,F)} for block P12=(A,C,E):on x=0: next states: EEC blk indices: 111 Pb10={(A,C,E)}=P12(no refinement) on x=1: next states: DBF blk indices: 222 Pb11={(A,C,E)}=P12(no refinement) P2={(A,C,E)}levelinputblk no.ENEE 644PS NS, z x=0 x=1A E, 0 D, 1B D, 0 F, 0C E, 0 B, 1D B, 0 F, 0E C, 0 F, 1F B, 0 C, 00/0BD0/01/00/01/11/0AF1/00/01/11/10/0EC0/0Example: Finding Equivalent States P1={(A,C,E),(B,D,F)} P2={(A,C,E)}for block P22=(B,D,F): on x=0: next states: DBB blk indices: 222 Pb20={(B,D,F)}=P22 on x=1: next states: FFC blk indices: 221 Pb21={(B,D),(F)}refine: P22=P22 •Pb21= Pb21 ={(B,D),(F)}P2={(A,C,E),(B,D),(F)}ENEE 644PS NS, z x=0 x=1A E, 0 D, 1B D, 0 F, 0C E, 0 B, 1D B, 0 F, 0E C, 0 F, 1F B, 0 C, 00/0BD0/01/00/01/11/0AF1/00/01/11/10/0EC0/0Example: Finding Equivalent States P1={(A,C,E),(B,D,F)}P2={(A,C,E),(B,D),(F)}for block P13=(A,C,E):on x=0: next states: EEC blk indices: 111 Pb10={(A,C,E)}=P13 on x=1: next states: DBF blk indices: 223 Pb11={(A,C),(E)}refine: P13=P13 •Pb11= Pb13 ={(A,C),(E)} P3={(A,C),(E)}ENEE 644PS NS, z x=0 x=1A E, 0 D, 1B D, 0 F, 0C E, 0 B, 1D B, 0 F, 0E C, 0 F, 1F B, 0 C, 00/0BD0/01/00/01/11/0AF1/00/01/11/10/0EC0/0Example: Finding Equivalent States P1={(A,C,E),(B,D,F)}P2={(A,C,E),(B,D),(F)}P3={(A,C),(E)}for block P23=(B,D):on x=0: next states: DB blk indices: 22 Pb10={(B,D)}=P23 on x=1: next states: FF blk indices: 33 Pb11 ={(B,D)}=P23P3={(A,C),(E),(B,D)}ENEE 644PS NS, z x=0 x=1A E, 0 D, 1B D, 0 F, 0C E, 0 B, 1D B, 0 F, 0E C, 0 F, 1F B, 0 C, 00/0BD0/01/00/01/11/0AF1/00/01/11/10/0EC0/0Example: Finding Equivalent States P1={(A,C,E),(B,D,F)}P2={(A,C,E),(B,D),(F)}P3={(A,C),(E),(B,D)}for block P33=(F): contains single state, cannot be partitioned.P3={(A,C),(E),(B,D),(F)}P3={(A,C),(E),(B,D),(F)}ENEE 644PS NS, z x=0 x=1A E, 0 D, 1B D, 0 F, 0C E, 0 B, 1D B, 0 F, 0E C, 0 F, 1F B, 0 C, 00/0BD0/01/00/01/11/0AF1/00/01/11/10/0EC0/0Example: Finding Equivalent States P1={(A,C,E),(B,D,F)}P2={(A,C,E),(B,D),(F)}P3={(A,C),(E),(B,D),(F)}One can compute P4 in the same way, which givesP4={(A,C),(E),(B,D),(F)}P4=P3 so we stopConclusion: A and C are equivalent B and D are equivalentENEE 6440/00/00/0BD0/00/0BD1/00/0D1/10/01/01/01/0AF0/01/11/10/01/01/00/00/0AFAF1/11/01/01/10/01/00/00/01/11/1EC1/10/00/00/00/0ECE0/0FSM Minimization with Equivalent States STG: collapse states in the same equivalent class to one state; update edges.Equivalent classes: (A,C), (B,D), (E), (F)ENEE 644Definition: Finite State MachineRecall: A Finite State Machine (FSM) of Mealy type is a 6 tuple <I,S,,S0,O,> I: input alphabet, a non-empty set of input values; S: a non-empty, finite set of states; : SxI S, a function defines the next state; S0: S, the set of initial/reset states; O: output alphabet; : SxI O, a function defines the output. ENEE 644FSM Equivalence CheckingM1=<I1,S1,1,S01,O1,1> M2=<I2,S2,2,S02,O2,2>What do we mean by M1 and M2 are equivalent? For any input, they should produce the same output.I1 = I2 O1 = O2 How to verify that M1 and M2 are equivalent? Assuming that S01={s01} and S02={s02}, then if there is no input string can distinguish s01 and s02, we claim that M1 and M2 are equivalent. ENEE 644The Product MachineThe product machine of two FSMs, M1=<I,S1,1,S01,O,1> and M2=<I,S2,2,S02,O,2>, is defined as M12=<I,S12,12,S012,{0,1},12> S12=S1xS2={(s1,s2)| s1S1,s2S2} 12: S12xI S12 12(s12,x)=t12=(t1,t2) 12(s12,x)=(1(s1,x), 2(s2,x)) =(t1,t2)S012 =S01xS02={(s01,s02)| s01S01,s02S02} 12: S12xI {0,1}12(s12,x)=1 iff 1(s1,x)=2(s2,x) M1 and M2 are equivalentM12always outputs 1. ENEE 644Run and Reachable StateFor an FSM M1=<I1,S1,1,S01,O1,1>, an input string x0x1…xk-1produces a sequence of states s0s1…sk(called a run, where s0 is the starting state)and an output string z0z1…zk-1. A state t is reachable from state s if there exists an input string that produces a run with s as the starting state and t as the ending state. The reachable states of an FSM <I,S,,S0,O,> is defined as: {tS| t is reachable from s, sS0} We only need to check the reachable states for FSM equivalence.ENEE 644FSM Equivalence CheckingM1=<I1,S1,1,S01,O1,1> M2=<I2,S2,2,S02,O2,2>If I1I2or O1 O2return not equivalent; Build the product machine M12; Start with the initial state s012, traverse the STG of the FSM M12; For each reachable state in M12, if it can output 0, return not equivalent; Return equivalent; To get a distinguishing sequence in the case of not equivalent, we need to store the predecessor information and do backtracking. ENEE 644x/1A,DA,Ex/1x/0x/0y/0y/1x/1B,FADy/1y/1•••C,FB,Ey/1y/1x/0x/0y/1y/1x/1y/0y/0CFBEx/0x/0Example: FSM Equivalence CheckingM1=<{x,y},{A,B,C},1,{A},{0,1},1> M2 =<{x,y},{D,E,F},2,{D},{0,1},2> M12=<{x,y},S12,12,{(A,D)},{0,1},12> |S12| = 9, however, only 3 states are reachable: (A,D),(B,E),(C,F) Every reachable state outputs 1 on all inputs. So M1 and M2 are equivalent. ENEE 644x/1A,DA,Ex/1x/0x/0y/0y/1x/1B,FADy/1y/1•••C,FB,Ey/1y/1x/0x/0y/1y/1x/0y/0y/0CFBEx/0x/1Example: FSM Equivalence CheckingNow, M1 and M2 are not equivalent. Consequently, one of the reachable state (C,F) outputs 0 on input x. Backtracking to find the distinguishing sequence. ENEE 644

We Need Your Support

Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks