Refinements

N.B. This section is incomplete and under construction

The mechanism of ``refinement'' in SMV allows one model to represent the behavior of a design simultaneously at many levels of abstraction. It also allows one to verify in a compositional manner that each level of the design is a correct implementation of the level above.

The basic object in the refinement system is a ``layer''. A layer is a named collection of assignments. For example:

        layer P : {
          x := y + z;
          next(z) := x;
        }

represents a layer named P, which contains assignments to signals x and z. Within a layer the single assignment rule applies. That is, any given signal may be assigned only once. However, a signal may be assigned in more than one layer.

One layer may be declared to ``refine'' another. The syntax for this declaration is:

        P refines Q;

where P and Q are names of layers. If P refines Q, then an assignment to any signal s in P supersedes the corresponding assignment to s in Q. For example, suppose that layer Q is defined as follows:

        layer Q : {
          y := z;
          next(z) := 2 * y;
        }

The net functional effect of these declarations is equivalent to:

        x := y + z;
        y := z;
        next(z) := x;

That is, the assignment to z in P supersedes the assignment to z in Q, because P refines Q. Any assignment that is superseded in this way becomes a part of the specification. That is, in our example, every trace of the system must be consistent with

        next(z) := 2 * y

at all times. This proposition is given the name ``z//Q'', meaning ``the assignment to signal z in layer Q''. Note that the property z//Q is true in the case of our example, since at all times

        x  =  y+z  =  z+z  =  2*z

Thus, we can infer that every trace of our system is also a trace of the system consisting only of the layer Q. Put another way, our system satisfies specification Q (and also, trivially, specification P).