[Next] [Up] [Previous] [Contents]

State machines

Here is an example of a small finite state machine, expressed in SMV. It starts in a state ``idle'' and waits for a signal ``start'' to be asserted. On the next cycle, it changes to a state ``cyc1'', then to state ``cyc2'', then returns to ``idle''. In state ``cyc2'', it asserts a signal ``done'':

        start,done : boolean;
        state : {idle,cyc1,cyc2};

        next(state) := 
          switch(state){
            idle: start ? cyc1 : idle;
            cyc1: cyc2;
            cyc2: idle;
          };

        done := (state = cyc2);

This illustrates two forms of conditional expressions in SMV. The ``switch'' operator evaluates its argument ``state'', then chooses the first expression in the curly brackets that is tagged with that value. Thus, if state = cyc1, then the value of the switch expression is cyc2. There is also a simpler form of conditional expression, that appears in the example as

        start ? cyc1 : idle

If ``start'' is true, this evaluates to ``cyc1'', else to ``idle''.

The above state machine can be expressed more ``procedurally'' using the structural conditional constructs describe in the next section. We would write:

        default done := 0;
        in switch(state){
          idle: 
            if start then next(state) := cyc1;
          cyc1: 
            next(state) := cyc2;
          cyc2:
            next(state) := cyc2;
            done := 1;
        }

This style of expression is semantically equivalent to the previous one, but can be much more readable for large complex state machines.