The MARCO/DARPA Gigascale SiliconResearch Center for Design & TestJune Workshop June 17th-18th, 2001Page 1Finite State Machines• Functional decomposition into states of operation• Typical domains of application:– control functions – protocols (telecom, computers, ...)• Different communication mechanisms:– synchronous EE249Fall071– (classical FSMs, Moore ‘64, Kurshan ‘90)– asynchronous– (CCS, Milner ‘80; CSP, Hoare ‘85)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, ortil th d i f t th t b ltEE249Fall072–until the driver fastens the seat belt, or – until the driver turns off the keyThe MARCO/DARPA Gigascale SiliconResearch Center for Design & TestJune Workshop June 17th-18th, 2001Page 2FSM ExampleKEY_ON => START_TIMERWAITEND_TIMER_5 => ALARM_ONKEY_OFF orBELT _ON =>END_TIMER_10 orBELT ON OFFEE249Fall073BELT_ON orKEY_OFF => ALARM_OFFIf no condition is satisfied, implicit self-loop in the current stateALARMFSM 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δ 2IS SSet of all subsets of I (implicit “and”)All other inputs are implicitly absentEE249Fall074δ : 2I×S → S e.g. δ( { KEY_OFF }, WAIT ) = OFFλ : 2I× S → 2Oe.g. λ ( { KEY_ON }, OFF ) = { START_TIMER }The MARCO/DARPA Gigascale SiliconResearch Center for Design & TestJune Workshop June 17th-18th, 2001Page 3Non-deterministic FSMsδ and λ may be relations instead of functions:δ ⊆2I×S×Sδ ⊆2S S e.g. δ({KEY_OFF, END_TIMER_5}, WAIT) = {{OFF}, {ALARM}}λ ⊆ 2I× S × 2O• Non-determinism can be used to describe:– an unspecified behavior(i l t ifi ti )implicit “and” implicit “or”EE249Fall075(incomplete specification)– an unknown behavior(environment modeling)• E.g. error checking first partially specified:NDFSM: incomplete specification• Then completed as even parity:BIT or not BIT => BIT or not BIT =>BIT or not BIT => ERRBIT or not BIT =>...SYNC =>not BIT =>BIT > ERR 01 7 817EE249Fall076BIT =>not BIT =>not BIT => ERR...SYNC =>not BIT =>...not BIT =>BIT =>BIT =>BIT => BIT => ERR p1p7d7d10 8The MARCO/DARPA Gigascale SiliconResearch Center for Design & TestJune Workshop June 17th-18th, 2001Page 4NDFSM: 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 orBELT ONEE249Fall07• Can be refined– E.g. introduce timing constraints– (minimum reaction time 0.1 s)s0BELT_ONNDFSM: time range• Special case of unspecified/unknown behavior, but so common to deserve special treatment for efficiency• E.g. delay between 6 and 10 s01 2 3 4START => SEC => SEC => SEC =>SEC =>START =>EE249Fall078056789SEC => ENDSEC =>SEC =>SEC =>SEC =>SEC => ENDSEC => ENDSEC => ENDThe MARCO/DARPA Gigascale SiliconResearch Center for Design & TestJune Workshop June 17th-18th, 2001Page 5NDFSMs and FSMs• Formally FSMs and NDFSMs are equivalent – (Rabin-Scott construction, Rabin ‘59)• In practice, NDFSMs are often more compact– (exponential blowup for determinization)s1s1ac accEE249Fall07s2s3s2,s3abas3bas2bas1,s3caFinite State Machines• Advantages:– Easy to use (graphical languages)– Powerful algorithms for– synthesis (SW and HW)– verification• Disadvantages:EE249Fall0710– Sometimes over-specify implementation– (sequencing is fully specified)– Number of states can be unmanageable– Numerical computations cannot be specified compactly (need Extended FSMs)The MARCO/DARPA Gigascale SiliconResearch Center for Design & TestJune Workshop June 17th-18th, 2001Page 6Modeling 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?EE249Fall0711FSM Composition• Bridle complexity via hierarchy: FSM product yields an FSM• Fundamental hypothesis: –all the FSMs change state together (synchronicity)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 + timerSTART TIMER >EE249Fall071201 2 3 456789START_TIMER =>START_TIMER =>SEC =>SEC => END_10_SECSEC => SEC =>SEC =>END_5_SECSEC =>SEC =>SEC =>SEC =>The MARCO/DARPA Gigascale SiliconResearch Center for Design & TestJune Workshop June 17th-18th, 2001Page 7FSM CompositionOFF, 0WAIT, 1KEY_ON and START_TIMER => START_TIMERmust be coherentSEC and OFF, 0WAIT, 1WAIT, 2not (KEY_OFF or BELT_ON) =>OFF, 1not SEC and (KEY_OFF or BELT_ON) =>SEC and (KEY_OFF or BELT_ON) =>EE249Fall0713OFF, 2BeltControlTimerFSM CompositionGiven M1 = ( I1, O1, S1, r1, δ1, λ1) and M2= ( I2, O2, S2, r2, δ2, λ2)Find the compositionM = ( I, O, S, r, δ, λ )given a set of constraints of the form:EE249Fall0714C = { ( o, i1, … , in) : o is connected to i1, … , in}The MARCO/DARPA Gigascale SiliconResearch Center for Design & TestJune Workshop June 17th-18th, 2001Page 8FSM Composition• Unconditional product M’ = ( I’, O’, S’, r’, δ’, λ’ )–I’ = I1 U I2–O’ = O1U O2–S’ = S1x S2–r’ = r1x r2δ’ = { ( A1, A2, s1, s2, t1, t2) : ( A1, s1, t1) εδ1and ( A2, s2, t2) εδ2}λ’ = { ( A1, A2, s1, s2, B1, B2) : ( A1, s1, B1) ελ1and EE249Fall0715( A2, s2, B2) ελ2}• Note:–A1 ⊆ I1, A2⊆ I2, B1⊆ O1, B2⊆ O2–2X U Y= 2Xx 2YFSM Composition• Constraint applicationλ {(AABB)λ’f ll( ii)CBBif dλ = { ( A1, A2, s1, s2, B1, B2) ελ’ : for all ( o, i1, … , in) εC o εB1UB2if and only if ijε A1U A2for all j }• The application of the constraint rules out the cases where the connected input and output have different values (present/absent).EE249Fall0716The MARCO/DARPA Gigascale SiliconResearch Center for Design & TestJune Workshop June 17th-18th, 2001Page 9I = I1 ∪ I2 O = O1 ∪ O2FSM CompositionFSM1FSM2i1i2oS = S1 × S2Assume that o1 ∈O1, i3 ∈I2, o1 =i3 (communication)δ and λ are such that, e.g., for each pair:δ1( { i1 }, s1 ) = t1, λ1( { i1 }, s1 ) = { o1 }12i3o1o2EE249Fall0717δ2( { i2, i3 }, s2 ) = t2, λ2( { i2 , i3 }, s2 ) = { o2 }we have:δ( { i1, i2, i3 }, ( s1, s2 ) ) = ( t1, t2 )λ( { i1, i2, i3 }, ( s1, s2 )
View Full Document
Unlocking...