Decomposing large data structures

In our trivial example, we are sending an array of 32 bytes. Because we only need to consider one bit out of each byte at a time, we were able to verify the implementation without explicitly decomposing this data structure. However, cases often arise when it is necessary to consider only one element at a time of a large structure. For example, we might increase the size of our array to 1 million bytes. As we will see later, sometimes even small arrays must be decomposed in this way. One one of decomposing a large array in the abstract model is to write an array of refinement maps (we'll see a more elegant way later, in section 4.6). Each element of this array defines a given low-level signal only when it contains the value of the corresponding element in the abstract array. For example, let's rewrite our interface data type to use a decomposed refinement map of this kind:

  module byte_intf(bytes){

    bytes : array INDEX of BYTE;

    valid : boolean;
    idx : INDEX;
    data : BYTE;

    forall(i in INDEX)
      layer spec[i]:
        if(valid & idx = i) data := bytes[i];
}

Notice that layer spec is now an array, with one element for each element of the array bytes. The layer spec[i] specifies the value of data only when idx is equal to i, and otherwise leaves data undefined. The advantage of this refinement map is that spec[i] refers to only one element of the array bytes. Thus, the other elements will not appear in the cone when verifying it, and we have reduced the number of state variables that the model checker must handle.

Let's go back to our 3-stage delay example, and use this new definition of byte_intf. Because we have changed the layer declarations, we also have to change the corresponding using...prove declarations. Replace these with the following:

  forall(i in INDEX){
    using stage2.valid//free, stage2.idx//free prove out.data//spec[i];
    using stage1.valid//free, stage1.idx//free prove stage2.data//spec[i];
  }

Now, when you try to open this file, you'll get an error message, something like this:

The implementation layer inherits two definitions of inp.data[5]
...in layer spec[31], "map7.smv", line 15
...in layer spec[30], "map7.smv", line 15
Perhaps there is a missing "refines" declaration?

This is because we have given many abstract definitions for inp.data without providing an implementation. By default, if there is only one abstract definition, SMV takes this as the implementation. However, if there are many abstract definitions, it is possible that these definitions are contradictory, and hence there is no possible implementation. There are several possible ways to make SMV stop complaining about this. One is to provide an actual implementation. For example, we could simply implement inp.data by a nondeterministic choice among all possible data values. This would mean, of course, that we could not then prove consistency with the maps inp.data//spec[i]. On the other hand, we don't really want to prove these, since they are actually assumptions about the inputs to our design, and not properties to be proved. One way to tell SMV this is to declare inp explicitly as an input to the design. SMV does not attempt to verify refinement maps driving global inputs. It just takes them as assumptions. If our main module is later used as a submodule in a later design, we'll have to verify these maps in the context of the larger design. Meanwhile, let's change the header of our main module to look like the following:

module main(bytes,inp,out){
  bytes : array INDEX of BYTE;
  input  inp : byte_intf(bytes);
  output out : byte_intf(bytes);

Notice we've also make bytes a parameter to the module. If we later use this module in a larger design, we can then specify what abstract data array we want the module instance to transmit. Now, open this file, and select, for example, property out.data[0]//spec[0]. You'll notice that there are now only 8 state variables in the cone, since 31 of data bits have been eliminated. Also, notice that SMV chose the layer spec[0] to define stage2.data[0], out of the 32 possible abstract definitions. This is a heuristic choice, which was made on the basis of the fact that we are verifying an abstraction in layer spec[0]. If you'd like to see the reasoning SMV went through to arrive at this choice, select the signal stage2.data[0] and pull down ``Abstraction|Explain Layer''.

If you now select ``Prop|Verify out.data[0]//spec[0]'', you can observe that the verification is in fact faster than in the previous case. However, you'll also notice that the number of properties to prove is now very large. In fact, it is 32 times greater than before, since every property has now been decomposed into 32 cases! Select ``Prop|Verify All'', and you will find that the total verification time for this long list of properties is about 15 seconds, actually longer than before. Surely it is unnecessary to verify all of the 32 cases for each refinement map, since each is in effect symmetric to all the others. In fact, if we simply tell SMV where the symmetry is, we can convince it to prove only one case out of 32.