** Next:** Decomposing large structures in
** Up:** Refinement verification
** Previous:** Decomposing large data structures
** Contents**

##

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
.

** Next:** Decomposing large structures in
** Up:** Refinement verification
** Previous:** Decomposing large data structures
** Contents**
2003-01-07