A very simple example

We will consider first a very simple example of specifying abstractions and refinement maps. Suppose that we would like to design a circuit to transmit an array of 32 bytes from its input to its output, without modifying the array. The abstract model in this case is just an unchanging array of bytes, since no actual operations are performed on the array. The refinement maps specify the protocol by which the array is transferred at the input and output. We'll assume the the input consists of three components: a bit valid indication the the input currently holds valid data, an index idx that tells which element of the array is currently being transferred, and a byte data that gives the value of this element. Assume the output uses a similar protocol. Thus far, we have the following specification:

typedef BIT 0..7;
typedef INDEX 0..31;
typedef BYTE array BIT of boolean;

module main(){

  /* the abstract model */
        
  bytes : array INDEX of BYTE;
  next(bytes) := bytes;  

  /* the input and output signals */

  inp, out : struct{
    valid : boolean;
    idx : INDEX;
    data : BYTE;
  }

  /* the refinement maps */

  layer spec: {
    if(inp.valid) inp.data := bytes[inp.idx];
    if(out.valid) out.data := bytes[out.idx];
  }

Note that the abstract model simply states that nothing happens to the array of bytes. The refinement map is partially specified. For example, if inp.valid is 0, then inp.data is allowed to have any value, since there is no else clause in the conditional. You can think of this as a ``don't care'' case in the specification.

Now let's add a very trivial implementation:

  init(out.valid) := 0;
  next(out) := inp;
}

That is, the output is just the input delayed by one time unit. Note, at time $t=0$ we have to signal that the output is not valid, but we don't have to specify initial values for idx and data since they are ``don't cares'' in this case.

Save this program in a file and open it with vw. Note that there are eight properties in the file, of the form out.data[i]//spec, where i = 0..7. Select property out.data[0]//spec, for example. If you click on the Cone tab, you'll notice that only signals with bit index 0 appear. This is because SMV has detected the property you selected doesn't depend on the other bit indices. Also notice that the data input signal inp.data[0] has used layer spec for its definition (since this is in fact the only available definition at this point). Thus, we are driving the input of our implementation from the abstract model (through a refinement map) and verifying the output with respect to the abstract model (again through a refinement map). Now, select ``Prop|Verify out.data[0]//spec''. It should take less than 2 seconds to verify this property. You can select ``Prop|Verify All'' to verify the remainder of the refinement maps. SMV will quickly recognize that the 7 remaining verification problems are isomorphic to the one we just solved, and report ``true'' for all of them. Note that although we have reduced the number of state bits by a factor of eight by using decomposition (since we only deal with one bit index at a time) we are still using 32 bits out of the data array for each verification. This gives us 39 state bits, which is a fairly large number and guarantees us at least 4 billion states. In this case, the large state space is easily handled by the BDD-based model checker, so we do not have to do any further decomposition. In general however, we cannot rely on this effect. Later we'll see how to decompose the problem further, so that we only use one bit from the data array.