Layers

A layer is a collection of abstract signal definitions. These are expressed as assignments in exactly the same way that the implementation is defined, except that they are bracketed by a layer statement, as follows:

  layer <layer_name> : {
        assignment1;
        assignment2;
        ...
        assignmentn;
  }

where each assignment is of the form

  <signal> := <expression>;

or

  next(<signal>) := <expression>;

or

  init(<signal>) := <expression>;

High level control structures, such as if, switch and for can also be used inside a layer construct, since these are simply ``syntactic sugar'' for assignments of the above form.

The layer declaration is actually a formal specification, which states that every implementation behavior must be consistent with all of the given assignments. If this is the case, we say the implementation refines the specification.

As an example, let's consider a very simple example of a specification and implementation of a finite state machine:

  module main(){
    x : boolean;

    /* the specification */

    layer spec: {
      init(x) := 0;
      if(x=0) next(x) := 1;
      else next(x) := {0,1};
    }

    /* the implementation */

    init(x) := 0;
    next(x) := ~x;
  }

Note that spec is not a keyword here - it is just an arbitrary name given to our specification. This specification is nondeterministic, in that at state 1, it may transition to either state 0 or state 1. The implementation on the other hand has only one behavior, which alternates between state 0 and state 1. Since this is one possible behavior of spec, the specification spec is satisfied.

If you enter this example into a file, and open the file with vw, you will find in the Properties page a single entry named x//spec. This is a notation for ``the definition of signal x in layer spec''. It appears in the Properties page because it is an obligation to be verified, rather than a part of the implementation. You can verify it by selecting ``Prop|Verify all''. SMV does this by translating the assignment into an initial condition and transition invariant. The former states that x is 0 at time $t=0$, while the latter states that the value of x at time $t+1$ is 1 if x is 0 at time $t$, and else is either 0 or 1. The implementation must satisfy these two conditions, which are verified by exhaustive search of the state space of the implementation.

If more than one signal is assigned in a layer, then the two definitions are verified separately. This is known as decomposition. The reason for using decomposition is that we may be able to use a different abstraction of the implementation to prove each component of the specification. As a very simple example, consider the following program:

  module main(){
    x,y : boolean;

    /* the specification */

    layer spec: {
      x := 1;
      y := 1;
    }

    /* the implementation */

    init(x) := 1;
    next(x) := y;
    init(y) := 1;
    next(y) := x;
  }

Both state bits in the implementation start at 1, and at each time they swap values. Thus, the specification is easily seen to be satisfied - both x and y are always equal to  1. If you open this example with vw, you will find two entries in the Properties page: x//spec and y//spec. Each of these can be verified separately (i.e., we can verify separately that x is always equal to 1 and that y is always equal to 1). Suppose we want to verify x//spec (select it in the Properties page). We now have two choices: we can use either the specification definition of y or the implementation definition y. Note, however, that if we use the specification definition of y, we eliminate one state variable from the model, since y is defined to be identically 1. Thus, by decomposing a specification into parts, and using one part as the ``environment'' for another, we have reduced the number of state variables in the model, and thus reduced the verification cost (though it is in any event trivial in this case). In fact, if you click on the Cone tab in vw, you will see that SMV has selected layer spec to define y, and that as a result, y is not a state variable. This is because SMV assumes by default that it is better to use an abstract definition of a signal than a detailed one. Select ``Prop|Verify x//spec'' to verify the property using this abstraction.

Note that y//spec can now be verified using x//spec to define x. This might at first seem to be a circular argument. However, SMV avoids the potential circularity by only assuming y//spec holds up to time $t-1$ when verifying x//spec at time $t$, and vice versa. Because of this behavior, we need not be concerned about circularities when choosing an abstract definition to drive a signal. SMV does the bookkeeping to insure that when all components of the specification are declared ``verified'', then in fact the implementation refines the specification.