Handling very large input files

SMV loads your entire input file or files, even if the property you intend to verify only depends on a very small section. Further, it ``flattens'' the entire description, meaning that it generates all the specified instances of modules explicitly. This can be quite time consuming if you are working with a large design at the ``RTL'' level, especially since the moudle hierarchy in such designes tends to be deep, and modules are used for very small elements such as individual ``flip-flops''.

You can speed up loading of a large design greatly by using the ``lazy flattening'' option. Using this option, SMV will only generate a module instance when it is actually needed, for example because a property you are proving depends on it. This can speed up the loading of a large design by one or two orders of magnitude.

To make efficient use of the option, you need to understand a little about the conditions that will force a module instance to be expanded. First, any module instance that contains an assert or layer must be expanded. This means that you should put all such declarations in modules that are close to the top of the hierarchy. Low level modules should only contain the following declarations:

• Type declarations
• Input and output declarations
• Assignments to variables
• Conditional and iterative constructs

In other words, the low level modules should only contain the description of your implementation, and not the proof. If this is the case, a low level module will only be instantiated if it assignes or declares some signal that is actually needed in proving some property.

There is one drawback to the ``lazy flattening'' approach. That is, it not practical using this option to check the entire program for circular definitions, since this would require flattening the entire design. This check is needed to make sure that these definitions are ``conservative'', and hence that the entire proof is valid. SMV skips the circularity check when using the ``lazy flattening'' option. This means that when all your properties are verified, you must run SMV once without lazy flattening to make sure your proof is valid. This will cause the entire design to be flattened, but need only be done once.

To use the lazy flattening option, put the following declaration at the top of your program:

option LazyFlatten=1;