Thus far, we've seen how we can decompose a large structure in the
abstract model (such as the byte array in our example), and verify
properties relating only to one small component of the structure. Now,
we'll consider the case where we have a large structure in the
implementation, and wish to consider only one component at a
time. Let's keep the specification from our previous example, but
design an implementation that has a large buffer that can store data
bytes in transit. To make the problem more interesting, we'll put flow
control in the protocol, so that our implementation can stop the flow
of incoming data when its buffer is full. To implement flow control,
we'll use two signals, one to indicate the sender is ready (`srdy`) and one to indicate the receiver is ready (`rrdy`). A byte
is transferred when both of these signals are true. Here's the definition
of this protocol as an interface data type:

module byte_intf(bytes){ bytes : array INDEX of BYTE; srdy,rrdy : boolean; idx : INDEX; data : BYTE; valid : boolean; valid := srdy & rrdy; forall(i in INDEX) layer spec[i]: if(valid & idx = i) data := bytes[i]; }Note that the refinement map only specifies the value of the data when both

module main(bytes,inp,out){ bytes : array INDEX of BYTE; input inp : byte_intf(bytes); output out : byte_intf(bytes); /* the abstract model */ next(bytes) := bytes;For the implementation, we'll define an array of 8 cells. Since all of the cells are symmetric, we'll define a scalarset type to index the cells:

scalarset CELL 0..7;Each cell holds an index and a data byte. Each cell also needs a bit to say when the data in the cell are valid:

cells : array CELL of struct{ valid : boolean; idx : INDEX; data : BYTE; }We also need pointers to tell us which cell is to receive the incoming byte and which cell is to send the outgoing byte:

recv_cell, send_cell : CELL;The implementation is ready to receive a byte when the cell pointed to by

inp.rrdy := ~cells[recv_cell].valid; out.srdy := cells[send_cell].valid;Here is the code that implements the reading and writing of cells:

forall(i in CELL)init(cells[i].valid) := 0; default{ if(inp.valid){ next(cells[recv_cell].valid) := 1; next(cells[recv_cell].idx) := inp.idx; next(cells[recv_cell].data) := inp.data; } } in { if(out.valid){ next(cells[send_cell].valid) := 0; } } out.idx := cells[send_cell].idx; out.data := cells[send_cell].data;For the moment, we will leave the pointers

Finally, having defined our implementation, we will define a refinement map for
the structure `cells` so that we do not have to consider the entire array
at once. In fact, this refinement map almost defines itself, given the way the
data structure `cells` is encoded. We want to say that if a cell `i`
is valid, then its data is equal to the element of `bytes` pointed to by
its index `idx`. Here is the refinement map:

forall(i in INDEX) layer spec[i]: forall(j in CELL) if(cells[j].valid & cells[j].idx = i) cells[j].data := bytes[i];Note that once again, we have decomposed the map into separate indices. If cell

Now that we have defined each cell's contents in terms of the abstract model, we
can verify each cell separately. We can then assume that all the cells are correct
when we verify the implementation output. Open this file, and notice that in the
properties pane, there are just two properties: `cells[0].data[0]//spec[0]` and
`out.data[0]//spec[0]`. All the other properties are equivalent to one of these
by symmetry. Try ``Prop|Verify All'' to check that in fact our refinement
is correct.
Now select `cells[0].data[0]//spec[0]` in the Properties pane, and
the click on the Cone tab. There are 15 state variables in total for this property.
Notice that once again SMV has chosen layer `spec[0]` to drive `inp.data[0]`,
since this is the layer we are verifying. Because of the decomposition we have used,
data bits from only one cell and one element of the `bytes` array appear in
the cone. In fact, most of the state bits come from the `valid` bits of the cells.
These are included in the cone because the bit `inp.rrdy` depends on them.
However, it is reasonable
to hypothesize that the correctness of cell 0 does not actually depend on the `valid`
bits of the other cells. We should be able to free them and still verify the property.
To do this, add the following declaration to the program:

forall(i in INDEX) forall(j in CELL) forall(k in BIT) using cells//free, cells[j] prove cells[j].data[k]//spec[i];This declaration probably requires some explanation. First, even though we are only interested in proving one property,

Open this version
and select
the property `cells[0].data[0]//spec[0]`. The number of state
variables should now be 8 rather than 15, since the `valid` bits
for the other cells are now free variables. Select ``Prop|Verify `cells[0].data[0]//spec[0]`'' and observe that our hypothesis is
confirmed - the correctness of cell 0 is preserved, even when we free
the state of the other cells. Also note that verification time is
reduced.

Note, that by freeing some signals, we have decreased the number of state variables in the cone, we have also increased the number of ``combinational'' variables. These are variables that act as free or constrained inputs to the model. We can go a step further and substitute the ``undefined'' value for these bits. This is very much like an ``X'' value in a logic simulator. For example:

0 & undefined = 0 1 & undefined = undefined 0 | undefined = undefined 1 | undefined = 1Using the undefined value has the advantage that no combinational variables will introduced, since these signals are given the constant value ``undefined''. The difficulty is that, as in a logic simulator, these undefined values can propagate widely, giving a pessimistic result - we may find that a counterexample is produced to the property using undefined values, even though the property is actually true. However, we can never ``prove'' a false property by introducing undefined values.

We can set signals to the undefined value using a predefined layer
called `undefined`. For example, replace `cells//free` in the
`using ... prove` declaration above with

cells//undefinedThis will cause the signals that were previously freed to be given the undefined value instead. Open the new file and select the property

Finally, let's go back to the other property we need to prove in this
example, which is that the outputs are correct with respect to the
specification (`out.data[0]//spec[0]`). Select this property in the
Properties pane, and observe that there are still 49 state variables in
the cone. This is because, although our refinement map drives the data value
for each cell from the abstract model, the control bits `idx` and `valid`
for each cell are still driven from the implementation. This is not a problem for
us, since BDD's come to our rescue in this case. You can confirm this by
selecting ``Prop|Verify `out.data[0]//spec[0]`''. This verification should
take less than 2 seconds. Nonetheless, if this were not the case, we could
reduce the number of state bits by freeing the cells' control bits. That is, our
refinement map provides that the data in a cell are correct, for any values of the
control bits `valid` and `idx`. So let's add the following declaration
to the program:

forall(i in INDEX) forall(j in CELL) forall(k in BIT) using cells[j].idx//free, cells[j].valid//free prove out.data[k]//spec[i];Open the new version and select the property