ELIMINATION OF ILLEGAL STATES WITHIN EQUIVALENCE CHECKING

A method for equivalence checking includes obtaining a first and a second representation for a semiconductor design and applying a set of inputs to both representations. The outputs of the first representation are compared to the outputs of the second representation. If a mismatch is found, the starting states for the first and second representations are evaluated using a model checker to see if they are reachable from a known legal state such as reset state for that representation. If both of the starting states are reachable, the mismatch is a real mismatch providing a counter-example of the equivalence of the two representations. If one or both of the starting states are unreachable, the mismatch is a spurious mismatch and the model checker can be used to generate an invariant to preclude those starting states in future iterations of the equivalence checker.