Decomposing large structures in the implementation

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 srdy and rrdy are true. Our system specification is exactly the same as before:

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 recv_cell is empty (i.e., not valid). On the other hand, it is ready to send a byte when the cell pointed to by send_cell is full (i.e., valid):

  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 recv_<cell and send_cell undefined, and thus completely nondeterministic. This will allow us to cover all possible policies for choosing cells. Later, we can refine these signals to use a particular policy (e.g., round-robin) without invalidating our previous work.

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 j's index is i, then cell j contains byte i from the abstract array.

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, cells[0].data[0]//spec[0], we give a prove declaration for cells[j].data[k]//spec[i], for all i,j,k. This is because we are not allowed to use constants of a scalarset type in the program. Second, in order to free the signals in all the cells except cell j, we specify cells//free, indicating that all components of cells should use the free layer, and then specify cells[j] to override this choice for the specific case of cell j. In a using declaration, a signal name without a layer indicates the implementation definition of that signal.

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  = 1

Using 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//undefined

This will cause the signals that were previously freed to be given the undefined value instead. Open the new file and select the property cells[0].data[0]//spec[0]. Notice in the Cone pane that the other valid bits are no longer combinational variables. Thus we have eliminated 7 combinational variables from the cone. On the other hand, you can observe by selecting ``Prop|Verify cells[0].data[0]//spec[0]'' that the property is still provable under this weaker assumption about the environment.

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 out.data[0]//spec[0]. Notice that the number of state bits is now reduced to 1, a single bit of the abstract array. The verification time is also reduced, as you can observe by selecting ``Prop|Verify out.data[0]//spec[0]''.