The MARCO DARPA Gigascale Silicon Research Center for Design Test June Workshop June 17th 18th 2001 Finite State Machines Functional decomposition into states of operation Typical domains of application control functions protocols telecom computers Different communication mechanisms synchronous classical FSMs Moore 64 Kurshan 90 asynchronous CCS Milner 80 CSP Hoare 85 1 EE249Fall07 FSM Example Informal specification If the driver turns on the key and does not fasten the seat belt within 5 seconds then an alarm beeps for 5 seconds or until til th the d driver i ffastens t th the seatt belt b lt or until the driver turns off the key 2 EE249Fall07 Page 1 The MARCO DARPA Gigascale Silicon Research Center for Design Test June Workshop June 17th 18th 2001 FSM Example KEY ON START TIMER WAIT KEY OFF or BELT ON OFF END TIMER 10 or BELT ON BELT ON or KEY OFF ALARM OFF END TIMER 5 ALARM ON ALARM If no condition is satisfied implicit self loop in the current state 3 EE249Fall07 FSM Definition FSM I O S r I KEY ON KEY OFF BELT ON END TIMER 5 END TIMER 10 END TIMER 10 O START TIMER ALARM ON ALARM OFF S OFF WAIT ALARM r OFF 2I S S Set of all subsets of I implicit and All other inputs are implicitly absent e g KEY OFF WAIT OFF 2I S 2 O e g KEY ON OFF START TIMER 4 EE249Fall07 Page 2 The MARCO DARPA Gigascale Silicon Research Center for Design Test June Workshop June 17th 18th 2001 Non deterministic FSMs and may be relations instead of functions 2I S S implicit and implicit or e g KEY OFF END TIMER 5 WAIT OFF ALARM 2I S 2O Non determinism can be used to describe an unspecified behavior i incomplete l t specification ifi ti an unknown behavior environment modeling 5 EE249Fall07 NDFSM incomplete specification E g error checking first partially specified 0 BIT or not BIT 1 BIT or not BIT BIT or not BIT ERR 7 8 BIT or not BIT SYNC Then completed as even parity not BIT 0 BIT p11 not BIT BIT d1 BIT not BIT p77 BIT ERR not BIT not BIT ERR d7 8 BIT SYNC 6 EE249Fall07 Page 3 The MARCO DARPA Gigascale Silicon Research Center for Design Test June Workshop June 17th 18th 2001 NDFSM unknown behavior Modeling the environment Useful to optimize don t care conditions verify exclude impossible cases E g driver model KEY ON or KEY OFF or BELT ON BELT ON s0 Can be refined E g introduce timing constraints minimum reaction time 0 1 s EE249Fall07 NDFSM time range Special case of unspecified unknown behavior but so common to deserve special treatment for efficiency E g delay between 6 and 10 s START 1 SEC 2 SEC 3 SEC 4 SEC START SEC END SEC END 9 SEC 8 8 0 SEC END SEC END SEC 6 7 5 SEC SEC EE249Fall07 Page 4 The MARCO DARPA Gigascale Silicon Research Center for Design Test June Workshop June 17th 18th 2001 NDFSMs and FSMs Formally FSMs and NDFSMs are equivalent Rabin Scott construction Rabin 59 In practice NDFSMs are often more compact exponential blowup for determinization s1 s1 a a b s2 c c s3 s1 s3 a c a c a s2 s3 a b s3 a b s2 EE249Fall07 Finite State Machines Advantages Easy to use graphical languages Powerful algorithms for synthesis SW and HW verification Disadvantages Sometimes over specify implementation sequencing is fully specified Number of states can be unmanageable Numerical computations cannot be specified compactly need Extended FSMs 10 EE249Fall07 Page 5 The MARCO DARPA Gigascale Silicon Research Center for Design Test June Workshop June 17th 18th 2001 Modeling Concurrency Need to compose parts described by FSMs Describe the system using a number of FSMs and interconnect them How do the interconnected FSMs talk to each other 11 EE249Fall07 FSM Composition Bridle complexity via hierarchy FSM product yields an FSM Fundamental hypothesis all the FSMs change state together synchronicity System state Cartesian product of component states state explosion may be a problem E g seat belt control timer START TIMER START TIMER START TIMER 0 12 SEC END 10 SEC SEC 1 SEC 2 SEC 9 SEC 3 SEC 8 4 SEC 7 SEC END 5 SEC SEC 6 5 EE249Fall07 Page 6 The MARCO DARPA Gigascale Silicon Research Center for Design Test June Workshop June 17th 18th 2001 FSM Composition KEY ON and START TIMER must be coherent START TIMER OFF 0 WAIT 1 not SEC and KEY OFF or BELT ON OFF 1 SEC and not KEY OFF or BELT ON WAIT 2 SEC and KEY OFF or BELT ON OFF 2 Timer Belt Control 13 EE249Fall07 FSM Composition Given M1 I1 O1 S1 r1 1 1 and M2 I2 O2 S2 r2 2 2 Find the composition M I O S r given a set of constraints of the form C o i1 in o is connected to i1 in 14 EE249Fall07 Page 7 The MARCO DARPA Gigascale Silicon Research Center for Design Test June Workshop June 17th 18th 2001 FSM Composition Unconditional product M I O S r I I1 U I2 O O1 U O2 S S1 x S2 r r1 x r2 A1 A2 s1 s2 t1 t2 A1 s1 t1 1 and A2 s2 t2 2 and A1 A2 s1 s2 B1 B2 A1 s1 B1 1 A2 s2 B2 2 Note A1 I1 A2 I2 B1 O1 B2 O2 2X U Y 2X x 2Y 15 EE249Fall07 FSM Composition Constraint application A1 A2 s1 s2 B1 B2 ffor allll o i1 in C only if ij A1 U A2 for all j o B1 U B2 if and d The application of the constraint rules out the cases where the connected input and output have different values present absent 16 EE249Fall07 Page 8 The MARCO DARPA Gigascale Silicon Research Center for Design Test June Workshop June 17th 18th 2001 FSM Composition I I1 I2 O O1 O 2 i1 i2 FSM1 S S1 S2 FSM2 o Assume that o1 O1 i3 I2 o1 i3 communication o 2 i3 1 and are such that e g for each pair 1 i1 s1 t1 1 i1 s1 o1 2 i2 i3 s2 t2 2 i2 i3 s2 o2 we have i1 i2 i3 s1 s2 t1 t2 i1 i2 i3 s1 s2 o1 o2 i e i3 is in input pattern iff o2 is in output pattern 17 EE249Fall07 FSM Composition Problem what if there is a cycle Moore machine depends on input and state only on state composition is always well defined Mealy machine and depend on input and state composition may be undefined what if 1 i1 s1 o1 but o2 2 i3 s2 i1 FSM1 o1 i3 FSM2 o2 Causality analysis in Mealy FSMs Berry 98 18 EE249Fall07 Page 9 The MARCO DARPA Gigascale Silicon Research Center for Design Test June Workshop June 17th 18th 2001 Moore vs Mealy Theoretically same computational power almost In practice different characteristics Moore machines non reactive response delayed by 1 cycle easy to compose always …
View Full Document
Unlocking...