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

The single assignment rule

In addition, SMV follows a ``single assignment'' rule. This means that a given signal can be assigned only once in a program. Thus, we avoid the problem of conflicting definitions. The definition of ``single assignment'' is compicated somewhat by the ``next'' and ``init'' operators. The rule is this: one may either assign a value to x, or to next(x) and init(x), but not both. Thus, the following are legal:

while the following are illegal:

An important note: assigning an array reference with a variable index counts as asigning every element in the array, as far as the single assignment rule is concerened. Thus, for example,

        x[0] := foo;
        x[count + 1] := bar;

is a violation of the single assignment rule, if ``count'' is not a constant. This is because it cannot be determined at compile time that ``count + 1'' is not equal to 0. One way to look at this, is that

        x[i] := foo;

(assuming ``i'' is not a constant) is considered to be exactly equivalent to

        if (i = 0) x[0] := foo;
        if (i = 1) x[1] := foo;
        if (i = 2) x[2] := foo;
        ...
        if (i = n) x[n] := foo;

(assuming x is declared array 0..n).

If you want to make two assignments to variable indices in the same array, use the ``default'' construct (described below). Thus

        default next(x[i]) := foo;
        in next(x[j]) := bar;

would be legal. In the case where i = j, the second assignment would take precedence.