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

breaking(ADDR) prove p;then variables of type

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

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

breaking(ADDR) prove impl_addr//L2; }This will cause SMV to treat

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.