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

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

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

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.