Using case analysis over data paths

Now we'll look at a slightly more complex example, to show how case analysis can be used to reduce a verification problem to a smaller one, by considering only one path that a given data item might take from input to output. This technique is quite useful in reasoning about data path circuitry.

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 out.idx = i & send_cell = j where i is an INDEX and k is a CELL. We can, in fact, have as many parameters in the case analysis as we like, provided we write the condition in the above form. SMV recognizes by the form of the expression that the cases are exhaustive.

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.