Debugging of counterexamples in formal verification
US8103999B1 · kind B1 · utility
Assignee
Inventor
Key dates
| Filing date | Jun 16, 2008 |
| Grant date | Jan 24, 2012 |
| Priority date | — |
| Expiry date | Jun 22, 2029 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
The result of a property based formal verification analysis of a circuit design may include at least one counterexample for each property that is violated, which a user can use to debug the circuit design. To assist the user in this debugging process, a debugging tool displays the counterexample trace annotated in such a way to illustrate where the property violation occurs and what parts of this trace contributes to the property violation. The debugging tool thus facilitates understanding of what parts of the counterexample trace are responsible for the property failure. The user can then select any of those contributing points as a starting point for further debugging.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.