Using case analysis over data paths

We'll use essentially the same specification as before, but in this case
our implementation will be the array of cells that we used previously
when discussing refinement maps (section 4.5).
We have an array of cells, and each incoming byte is stored in an
arbitrarily chosen cell. Recall that the specification in this case
has to take into account the handshake signals. That is, the data
are only valid when both `sdry` and `rrdy` are true:

/* the abstract model */ bytes : array INDEX of BYTE; next(bytes) := bytes; /* the input and output signals */ inp, out : struct{ srdy,rrdy : boolean; idx : INDEX; data : BYTE; } /* the refinement maps */ layer spec: { if(inp.srdy & inp.rrdy) inp.data := bytes[inp.idx]; if(out.srdy & out.rrdy) out.data := bytes[out.idx]; }

For reference, here is the implementation again:

/* the implementation */ cells : array CELL of struct{ valid : boolean; idx : INDEX; data : BYTE; } recv_cell, send_cell : CELL; inp.rrdy := ~cells[recv_cell].valid; out.srdy := cells[send_cell].valid; forall(i in CELL)init(cells[i].valid) := 0; default{ if(inp.srdy & inp.rrdy){ next(cells[recv_cell].valid) := 1; next(cells[recv_cell].idx) := inp.idx; next(cells[recv_cell].data) := inp.data; } } in { if(out.srdy & out.rrdy){ next(cells[send_cell].valid) := 0; } } o out.idx := cells[send_cell].idx; out.data := cells[send_cell].data;

Recall that in the previous example, we wrote refinement maps for the data in the individual cells, in order to break the verification problem into two pieces: one to show that cells get correct data, and the other to show that data in cells are correctly transfered to the output. Now, we will use case analysis to get a simpler decomposition, with only one property to prove.

Our case analysis in this example will be a little finer. That is because
we have two arrays we would like to decompose. One is the array of
bytes to transfer, and the other is the array of cells. We would like to
consider separately each case where `byte[i]` gets transfered
through `cell[j]`. In this way, we can consider only one byte and
one cell at a time. This is done with the following declaration:

forall (i in INDEX) forall (j in CELL) subcase spec_case[i][j] of out.data//spec for out.idx = i & send_cell = j;Notice that our case analysis now has two parameters. Each case is of the form

Now run this example, and observe that once again,
we have a single property to prove: `out.data//spec_case[0][0]`. The other cases are symmetric. If you
look in the cone, you'll see that, while all elements of `bytes`
and `cells` are referenced, all except element 0 of these arrays
is left undefined, according to SMV's default heuristic. This makes
the verification problem small enough that we can handle it directly,
without resorting to an intermediate refinement map. You can confirm
this by verifying `out.data//spec_case[0][0]`.

This technique of breaking into cases as a function of the specific path taken by a data item through a system is the most important reduction in using SMV to verify data path circuitry. Notice that symmetry is crucial to this reduction, since without it we would have a potential explosion in the number of different paths.