Symbolic simulation as a simplifying strategy for SoC verification

The successful application of model-checking to industrial designs requires methods for reducing the complexity of the model. This paper presents an original strategy, for a well identified class of circuit behaviors; by running an appropriate symbolic simulation pattern before the actual proof of a temporal formula, an important FSM model simplification can be obtained. The actual model reduction step is formalized and illustrated. This method has been implemented within the CMU version of the SMV model checking tool and validated on a large industrial design.