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

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

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 , while the latter
states that the value of `x` at time is 1 if `x` is 0 at time , 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

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 when verifying `x//spec`
at time , 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.