The circular dependency rule

If we have the assignment

        x := y;

then we say that x depends on y. A combinational loop is a cycle of dependencies that is unbroken by delays. For example, the assignments

        x := y;
        y := x;

form a combinational loop. Although as equations, they may have a solution, there is no fixed order in which we can compute x and y, since the $i$th value of x depends on the $i$th value of $y$ and vice versa.

To be more precise, an assignment of form

        next(x) := <expr>;

introduces ``unit delay dependencies''. There is a unit delay dependency from x to every signal referenced in <expr>. An assignment of the form

        <signal> := <expr>;

introduces ``zero delay dependencies'', in the same way. A combinational loop is a cycle of dependencies whose total delay is zero. Combinational loops are illegal in SMV.

Therefore, legal SMV programs have the following property: for any sequence values chosen for the unassigned (free) signals, there is at least one solution for the assigned signals. There may be multiple solutions in the case where a signal has an unassigned initial value, or the case of nondeterministic assignments (see below).

There are cases where a combinational loop ``makes sense'', in that there is always a solution of the equations. In this case, the order in which signals are evaluated may be conditional on the values of some signals. For example, take the following system:

        x := c ? y : 0;
        y := ~c ? x : 1;

If c is false, then we may first evaluate x, then y, obtaining x = 0, then y = 0. On the other hand, if c is true, we may first evaluate y, then x, obtaining y = 1, then x = 1. The existence of conditional schedules such as this is difficult to determine, since it may depend on certain states (or signal values) being ``unreachable''. For example, if we have

        x := c ? y : 0;
        y := d ? x : 1;

it may be the case that c and d are never true at the same time, in which case x and y can always be evaluated in some order. Loops of this kind do sometimes occur in hardware designs (especially in buses and ring-structured arbiters). It is possible that at a future time the definition of a combinational to could be relaxed in order to allow such definitions. Currently, however, combination loops are defined only in terms of syntactic dependencies.