next up previous contents
Next: State machines Up: Signals and assignments Previous: Assignments   Contents

Unit delay assignments - the ``next'' operator

A special operator is provided for describing recurrences. Recurrences are circular or recursive systems of equations, and are the way that sequential systems are described in SMV.

If x is a signal, then next(x) is, intuitively, the ``next'' value of x. More precisely, the $i$th value of next(x) is equal to the $(i+1)$st value of x. Thus, for example, if

              x = 0,1,2,3,...
then

        next(x) = 1,2,3,4,...

By assigning a value to the ``next'' value of a signal, we can define a sequential machine. For example, assuming x and y are boolean signals,

        next(x) := y ^ x;
defines a signal x which ``flips'' each time the signal y is true (the ^ operator stands for ``exclusive or''). By definition, the ``next'' value of x is equal to (y ^ x), which is equal to x if y is false and ~x if y is true. Note, however, that the above assignment does not tell us the initial value of x. Thus, we obtain a different sequence depending on whether x starts at 0 or 1. We can determine this initial value by assigning

        init(x) := 0;

In this case, if we had

        y = 0;1;0;1;...
we would get

        x = 0;0;1;1;0;0;1;1;...

On the other hand, if we assigned

        init(x) := 1;
we would obtain the sequence

        x = 1;1;0;0;1;1;0;0;...

As another example, to declare a signal x that maintains a running sum of the values of a signal y, we would say

        init(x) := 0;
        next(x) := x + y;


next up previous contents
Next: State machines Up: Signals and assignments Previous: Assignments   Contents
2002-10-28