A slightly larger example

Now, let's reconsider the example from the previous section of an implementation with an array of cells (section 4.6.2). For reference, here are the specification and implementation:

  /* 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.