We will consider first a very simple example of specifying abstractions
and refinement maps. Suppose that we would like to design a circuit to
transmit an array of 32 bytes from its input to its output, without modifying
the array. The abstract model in this case is just an unchanging array
of bytes, since no actual operations are performed on the array. The refinement
maps specify the protocol by which the array is transferred at the input
and output. We'll assume the the input consists of three components:
a bit `valid` indication the the input currently holds valid data, an
index `idx` that tells which element of the array is currently being transferred,
and a byte `data` that gives the value of this element. Assume the output uses
a similar protocol. Thus far, we have the following specification:

typedef BIT 0..7; typedef INDEX 0..31; typedef BYTE array BIT of boolean; module main(){ /* the abstract model */ bytes : array INDEX of BYTE; next(bytes) := bytes; /* the input and output signals */ inp, out : struct{ valid : boolean; idx : INDEX; data : BYTE; } /* the refinement maps */ layer spec: { if(inp.valid) inp.data := bytes[inp.idx]; if(out.valid) out.data := bytes[out.idx]; }

Note that the abstract model simply states that nothing happens to the
array of bytes. The refinement map is partially specified. For
example, if `inp.valid` is 0, then `inp.data` is allowed to
have any value, since there is no `else` clause in the conditional.
You can think of this as a ``don't care'' case in the specification.

Now let's add a very trivial implementation:

init(out.valid) := 0; next(out) := inp; }That is, the output is just the input delayed by one time unit. Note, at time we have to signal that the output is not valid, but we don't have to specify initial values for

Save this program in a file and open it
with `vw`. Note that there are
eight properties in the file, of the form `out.data[i]//spec`, where
`i = 0..7`. Select property `out.data[0]//spec`, for example.
If you click on the Cone tab, you'll notice that only signals with bit index 0
appear. This is because SMV has detected the property you selected doesn't depend
on the other bit indices. Also notice that the data input signal `inp.data[0]`
has used layer `spec` for its definition (since this is in fact the only
available definition at this point). Thus, we are driving the input of our
implementation from the abstract model (through a refinement map) and verifying
the output with respect to the abstract model (again through a refinement map).
Now, select ``Prop|Verify `out.data[0]//spec`''. It should take less than
2 seconds to verify this property. You can select ``Prop|Verify All'' to verify
the remainder of the refinement maps. SMV will quickly recognize that the 7 remaining
verification problems are isomorphic to the one we just solved, and report ``true''
for all of them. Note that although we have reduced the number
of state bits by a factor of eight by using decomposition (since we only deal with
one bit index at a time) we are still using 32 bits out of the data array for
each verification. This gives us 39 state bits, which is a fairly large number and
guarantees us at least 4 billion states. In this case, the large state space is easily
handled by the BDD-based model checker, so we do not have to do any further decomposition.
In general however, we cannot rely on this effect. Later we'll see how to decompose
the problem further, so that we only use one bit from the data array.