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 described 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. The conditional constructs are only syntactic however, and can always be viewed as an abbreviation for a collection of simple assignment statements.