/* the specification */ layer spec: { if(inp.srdy & inp.rrdy) inp.data := bytes[inp.idx]; if(out.srdy & out.rrdy) out.data := bytes[out.idx]; } /* 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; } } out.idx := cells[send_cell].idx; out.data := cells[send_cell].data;

Let's make just one change to the source: we'll redefine the scalarset types INDEX and CELL to have undefined range:

scalarset INDEX undefined; scalarset CELL undefined;

Since these types have undefined ranges, SMV will choose a data type
reduction for use (though, of course, we could specify one if
we wanted to). Now, run this modified version.
You'll notice that in the properties pane, we have just one property
to prove, as before: `out.data//spec_case[0][0]`. In the cone pane,
observe that the variables of type `INDEX` and `CELL` have
only one boolean variable encoding them (representing the value 0 and `NaN`).
In addition, only `cell[0]` and `byte[0]` appear. This is because
SMV chose to reduce the types `INDEX` and `CELL` to contain only
those values appearing in the property being verified, which in this case
are just the value 0 for both types. Confirm that in fact the specification
can be verified using this reduction.

Note that the proof reduction that we used for the case of a fixed number of cells and a fixed number of bytes, worked with no modification when we switched to an arbitrary number of bytes and cells!

These very simple examples provide a paradigm of the verification of complex hardware systems using SMV. One begins by writing refinement maps. They specify the inputs and outputs of the system in terms of a more abstract model, and possibly specify internal points as well, to break the verification problem into parts. The resulting properties are then broken into cases, generally as a function of the different paths that a data item may take from one refinement map to another. These cases are then reduced to a tractable number by symmetry considerations. Finally, for each case, a data type reduction is chosen which reduces the large (or even infinite) data types to a small fixed number of values. The resulting verification subproblems are then handled by symbolic model checking.