Exploiting Symmetry

Change the type declaration for INDEX from

typedef INDEX 0..31;

to

scalarset INDEX 0..31;

This is exactly the same as an ordinary type declaration, except it tells SMV that the given scalar type is symmetric, in the sense that exchanging the roles of any two values of the type has no effect on the semantics of the program. In order to ensure that this symmetry exists, there are a number of rules placed on the use of variables of a scalarset type. For example, we can't use constants of a scalarset type, and the only operation allowed on scalarset quantities is equality comparison. In addition, we can't mix scalarset values with values of any other type. We can, however, declare an array whose index type is a scalarset. This makes it legal for us to make the type INDEX into a scalarset. Now, when SMV encounters an array of properties whose index is of scalarset type, it chooses only one case to prove, since if it can prove one case, then by symmetry it can prove all of them.

Let's see the effect of this on our example. Open the new file (with INDEX changed to a scalarset), and look in the Properties page. You'll see that there are now only properties from layer spec[0]. Pull down ``Prop|Verify All'', and you'll find the total verification time reduced to about a half second (a savings of a factor 32!).

We can go a step further than this, and make the type BIT a scalarset as well. This is because all of the bits within a byte are symmetric to each other. So change

typedef BIT 0..7;

to

scalarset BIT 0..7;

and open the new file. Now, in the Properties pane, there are only three properties, one for each stage! Thus, using symmetry, we have reduced the number of properties, by a factor of $32\times 8 = 256$.