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 supercedes 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 supercedes the assignment to z
in Q, because P refines Q. Any assignment that is superceded 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 * yat 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*zThus, 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).