Assignments

An assignment is of the form

        <signal> := <expr>;

where <expr> is an expression that combines other signals using operators like ~ and &. Unlike an assignment in a typical ``procedural'' language, this assignment means exactly what it says: that <signal> is equal to <expr>. So for example, suppose we make the assignment

        zip := foo & bar;

If foo and bar are as above, then

                 zip = 0;0;0;1;...

The assignments in an SMV program are interpreted as equations holding simultaneously. That is, the fact that two assignments occur in sequence in a program is not interpreted to mean that they are to hold sequentially. Thus, for example, if these assignments appear in a program:

  y := x + 1;
  z := y + 1;

then we have (at all times) z = x + 2.