USING LOCAL REDUCTION IN MODEL CHECKING TO IDENTIFY FAULTS IN LOGICALLY CORRECT CIRCUITS

A method and computer program for verifying a design of a circuit comprises selecting a portion of a model of the design having a plurality of inputs and outputs; providing a property for the design that defines a predetermined behavior of one or more of the outputs; determining whether a stimulus exists that, when applied to the inputs of the portion, can produce a behavior other than the predetermined behavior at the outputs of the portion; when the stimulus exists, determining whether the model of the design of the circuit can produce the stimulus at the inputs of the portion of the model of the circuit; and when the stimulus cannot be produced by the model of the design of the circuit at the inputs of the portion of the model of the circuit, preserving a description of the stimulus for analysis.