Rules for assignments

An SMV program amounts simply to a system of simultaneous equations, with a set of unknowns that are the declared signals. With an arbitrary set of equations, there is, of course, no guarantee that a solution exists, or that the solution is unique. Examples of systems that have no solutions are

        x := x + 1;

or

        next(x) := x + 1;
        next(x) := x - 1;

An example of a system with many solutions is

        x := y;
        y := x;

We avoid these difficulties by placing certain rules on the structure of assignments in a program. These rules guarantee that every program is ``executable''. This means, among other things, that a schedule must exist for computing the elements of all the sequences. The rules for assignments are:

• The single assignment rule - each signal may be assigned only once.
• The circular dependency rule - a program may not have ``cycles'' in its dependency graph that are not broken by delays.