Patent ReferencesMethod for the automatic generation of test sequences Efficient regression verification System and method for model size reduction of an integrated circuit utilizing net invariants Method for automatically generating behavioral environment for model checking Method and apparatus for diagnosing failure occurrence position Patent #: 6205559 InventorsApplicationNo. 404281 filed on 09/23/1999US Classes:714/32, Particular stimulus creation703/13, SIMULATING ELECTRONIC DEVICE OR ELECTRICAL SYSTEM703/14, Circuit simulation703/15, Including logic703/16, Event-driven714/33, Derived from analysis (e.g., of a specification or by stimulation)714/724, Digital logic testing714/741, Simulation716/4, Testing or evaluating716/5Design verification (e.g., wiring line capacitance, fan-out checking, minimum path width)ExaminersPrimary: Beausoliel, RobertAssistant: Maskulinski, Michael Attorney, Agent or FirmInternational ClassH02H 003/05AbstractA method of verifying a digital circuit in which state transition information is extracted from the output of a non-formal first verification technique. A formal verification tool is then applied to the extracted state transition information to extend the verification coverage of the digital circuit beyond the coverage that is achieved using the first verification technique. In one embodiment, the method includes the initial step of applying a first verification technique such as a simulation technique to a model of the digital circuit. In the preferred embodiment, the application of the formal verification tool comprises applying a model checker to the extracted state transition data to achieve a formal verification of the state machine represented by the state transition diagram. In one embodiment, the extracted state transition information includes a set of data points each representing a present state, a present input, and a next state. In one embodiment useful for extending the verification coverage provided by a conventional non-formal verification technique, the non-formal tool is used to verify satisfaction of a specification or rule by traversing a first transition path of the circuit. The non-formal tool is then used a second time to verify the rule or specification by traversing a second transition path. State transition information generated during the first and second passes of the non-formal verification technique is then extracted and provided to a formal verification tool such as a model checker. The formal verification of the circuit represented by the extracted state transition information extends the verification coverage achieved with the non-formal verification tool such as by, for example, traversing the digital circuit with a third transition path that was not explored with the non-formal verification tool. In addition, infinite loop conditions or live lock conditions may be detected by applying the formal verification technique to the extracted state transition information. Extraction and archiving of transition information may be performed periodically to accumulate new transition information.Other References
Field of SearchState validity checkParticular stimulus creation Derived from analysis (e.g., of a specification or by stimulation) Simulation Digital logic testing Including logic SIMULATING ELECTRONIC DEVICE OR ELECTRICAL SYSTEM Circuit simulation Event-driven Testing or evaluating Design verification (e.g., wiring line capacitance, fan-out checking, minimum path width) | |