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

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 ith value of x depends on the ith 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 refernced 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. Currently, 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 certains 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). The expected approach to this problem is require the user to provide constraints on the order of evaluation (so that the program can be compiled), and to verify that these constraints always have a solution. Currently, however, combination loops are simply disallowed.

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