Using local reduction in model checking to identify faults in logically correct circuits

A computer program stored on a tangible computer medium embodying instructions executable by a computer for verifying a design of a circuit, the computer program comprising:

• selecting a first portion of a model of the design, wherein the first portion has a plurality of first inputs and outputs;
• providing a property for the design, wherein the property defines a predetermined behavior of one or more of the first outputs;
• determining whether a first stimulus exists that, when applied to the first inputs, can produce a behavior other than the predetermined behavior at the one or more first outputs;
• when the first stimulus exists, determining whether the model can produce the first stimulus at the first inputs;
• and
• when the stimulus cannot be produced by the model at the first inputs, preserving a first description of the first stimulus for analysis.

A method for verifying a design of a circuit, comprising:

• selecting a portion of a model of the design, wherein the portion has a plurality of inputs and outputs;
• providing a property for the design, wherein the property defines a predetermined behavior of one or more of the outputs;
• determining whether a stimulus exists that, when applied to the inputs, can produce a behavior other than the predetermined behavior at the one or more outputs;
• determining whether the model can produce the stimulus at the inputs based on said stimulus existence determination;
• and
• preserving a description of the stimulus for analysis when the stimulus cannot be produced by the model.