Efficient mechanism of fault qualification using formal verification
AssigneeSynopsis, Inc.
InventorsSandeep Jana, Arunava Saha, Pratik Mahajan, Per Bjesse, Alfred Koelbl
Life of this patent
Estimating the term…
Abstract
The fault analysis problem is modelled by automatically creating additional properties (fault properties) and constraints based on a plurality of injected faults and existing user assertions. These fault properties and constraints are sent to formal verification in a single run to qualify all of the faults together, rather than sequentially checking each fault in a separate formal verification run.
Claims20
A method implemented on a computer system comprising a processor, the processor executing instructions to effect a method for checking an adequacy of user assertions in a formal verification environment that tests a functionality of a design for an integrated circuit, the method comprising:
- injecting a plurality of faults into the design for the integrated circuit;
- and
- creating a plurality of fault properties based on the plurality of injected faults and the user assertions, wherein the plurality of fault properties are suitable for addition to the formal verification environment, all of the plurality of fault properties can be evaluated in a single run of the formal verification environment, and an evaluation of the plurality of fault properties indicates whether the user assertions are adequate to detect the plurality of injected faults.
A method implemented on a computer system comprising a processor, the processor executing instructions to effect a method for checking an adequacy of user assertions in a formal verification environment that tests a functionality of a design for an integrated circuit, the method comprising:
- injecting a plurality of faults into the design for the integrated circuit;
- creating a fault property for the formal verification environment for each injected fault of the plurality of injected faults, wherein the fault property corresponding to said each injected fault asserts that enabling the injected fault implies that none of the user assertions are violated;
- creating a stability constraint for the formal verification environment, the stability constraint specifying that if any injected fault is enabled then it remains enabled for an entire run of the formal verification environment and if any injected fault is disabled then it remains disabled for the entire run of the formal verification environment;
- and
- creating a one-hot constraint for the formal verification environment, the one-hot constraint specifying that if any injected fault is enabled then all the other injected faults are disabled;
- wherein all of the fault properties can be evaluated in a single run of the formal verification environment subject to the stability constraint and to the one-hot constraint.
A system for checking an adequacy of user assertions in a formal verification environment that tests a functionality of a design for an integrated circuit, the system comprising:
- a first computer module that:
- injects a plurality of faults into the design for the integrated circuit;
- creates a fault property for the formal verification environment for each injected fault of the plurality of injected faults, wherein the fault property corresponding to each injected fault asserts that enabling the injected fault implies that none of the user assertions are violated;
- creates a stability constraint for the formal verification environment, the stability constraint specifying that if any injected fault is enabled then it remains enabled for an entire run of the formal verification environment and if any injected fault is disabled then it remains disabled for the entire run of the formal verification environment;
- and
- creates a one-hot constraint for the formal verification environment, the one-hot constraint specifying that if any injected fault of the plurality of injected faults is enabled then all the other injected faults of the plurality of injected faults are disabled;
- and
- a second computer module that:
- executes a single run of the formal verification environment that includes the plurality of fault properties, the stability constraint and the one-hot constraint;
- wherein all of the plurality of fault properties are evaluated in the single run of the formal verification environment subject to the stability constraint and to the one-hot constraint.
Dependencies are inferred from the claim text.