Bit vectors as scalarsets

In previous examples using symmetry, we have modeled data values and array indices as completely symmetric types, which allowed us to reduce the verification problem down to a few representative cases. However, in practice, these type will be implemented in hardware as bit vectors. This presents a dilemma: at the high level, we would like to model these types as scalarsets, but at the implementation level we may need to reference the individual bits of that represent them. For example, to implement the ALU function on data words, we might like to be able to write a bit-level adder. As another example, though it may be feasible almost everywhere to treat a 32 bit ``address'' as a scalarset, there may a place in the implementation where an address is broken into high and low order words, for multiplexed transmission. This operation cannot be performed on a scalarset.

To address this problem, SMV supports bit vectors as scalarset types. This allows us to look at a given type either as a fully symmetric set of integers (a scalarset), or as a bit vector, depending on which representation is most convenient. For example, here is a declaration of a bit vector scalarset:

    scalarset ADDR array 31..0 of boolean;

In general, arrays of booleans of any size can be scalarset types. Now, suppose we are proving a property ``p''. If we choose not to break the symmetry of the type ADDR, then variables of type ADDR will be treated as integers in the range $0..2^{32}-1$. On the other hand, if we choose to break the symmetry of type ADDR using the declaration:

    breaking(ADDR) prove p;

then variables of type ADDR are treated as arrays of 32 bits. That means, in particular, that we can break properties about addresses down into properties of the individual bits.

As an example of this, suppose that we have a read-only memory array, whose addresses are 24 bits, but the address is multiplexed into the ROM in two 12-bit hunks. At a high level, we would like to model this as a lookup in an array, such that addresses are treated in a completely symmetric way. However, at the implementation level, we need to be able to refer to the individual bits of address. We begin by declaring addresses to bit 24-bit scalarsets:

  scalarset ADDR array 23..0 of boolean;

We'll assume some type WORD of data words is also defined. For example, a word could be a 32-bit quantity:

  typedef WORD array 31..0 of boolean;

We won't need to exploit the symmetry of data words for this example.

The high level model is quite straightforward:

  module main(){

    ROM : array ADDR of WORD;

    stall : boolean;
    addr_inp : ADDR;
    data_out : WORD;

    next(ROM) := ROM;   /* ROM stays constant over time */

    layer L1:
      if(~stall)
        data_out  := ROM[addr_inp];

    /* assume the address input is held while we stall */
    if(stall)
      next(addr_inp) := addr_inp;
    else next(addr_inp) := undefined;

In the implementation, we'll use a two-state finite state machine to determine whether the high word or low word of the address is being clocked into the ROM. We stall the abstract model when in the low word state:

    state : {tx_low, tx_high};

    init(state) := tx_low;
    if(state = tx_low){
      next(state) := tx_high;
    }
    else next(state) := tx_low;

    stall := (state = tx_low);

We'll also need a 12 bit register to save the low word of the address while the high word is being transmitted:

    low_reg : array 11..0 of boolean;
    breaking(ADDR)
      if(state = tx_low)
        next(low_reg) := addr_inp[11..0];

Note that in order to extract the low order 12 bits of the address, we have to declare that we're breaking the symmetry of type ADDR. Otherwise SMV will report an error. Now, we reassemble the address from the high and low order parts, and look up in the array:

    impl_addr : ADDR;
    breaking(ADDR)
      impl_addr := addr_inp[23..12] :: low_reg;

    data_out := ROM[impl_addr];

Now, of course, we want to show that the value of data_out produced by this implementation actually satisfies the specification in layer L1. To handle the lookup in the ROM array, we have to rely on the symmetry of type ADDR, since we cannot possibly check $2^{24}$ cases separately. However, the lookup in the ROM array depends on impl_addr, which breaks the symmetry. Therefore, we will write a refinement map for impl_addr, breaking the problem into two parts, one which breaks the symmetry of ADDR, and one which does not:

    layer L2:
      if(state=tx_high) impl_addr := addr_inp;

That is, we rely on the fact that the address reassembled from the high and low parts must equal the original address. Now, to prove the data output correctness, we do the usual trick of splitting cases on the address:

   forall(a in ADDR) subcase L1[a] of data_out//L1 for addr_inp = a;

To verify the refinement relation for impl_addr, however, we simply break the symmetry of addresses:

   breaking(ADDR) prove impl_addr//L2;
 }

This will cause SMV to treat impl_addr as a 24-bit vector when proving this property. As a result, we will have to verify each bit if impl_addr separately. This is not a problem, however, since the verification problem for each bit is trivial.

Now, open this example, and observe the ``Cone'' pane. You'll notice that there are 32 instances of the data output correctness property data_out//L1, one for each bit in the data path. However, only one representative address case was chosen because we are exploiting the symmetry of addresses. Similarly, there are 24 instance of the refinement relation impl_addr//L2, one for each address bit. This is because we are breaking the symmetry of addresses to prove this property, hence addresses appear as bit vectors. If you select ``Verify all'', you'll find that the model checking goes very quickly, because all 32 data cases are isomorphic, as are all 12 cases for each of the low and high halves of the address word. Thus, all but three instances hit in SMV's hash table.

Thus, we have been able to verify a property involving a 24-bit address space, by exploiting symmetry of the bit vector type ADDR to deal with the large memory array, but breaking the symmetry when verifying the bit-level multiplexing if the address.