Method and system for enhanced verification by closely coupling a structural overapproximation algorithm and a structural satisfiability solver
US7356792B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Jan 26, 2006 |
| Grant date | Apr 8, 2008 |
| Priority date | — |
| Expiry date | Apr 29, 2026 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method, system and computer program product for performing verification are disclosed. A first abstraction of an initial design netlist containing a first target is created and designated as a current abstraction, and the current abstraction is unfolded by a selectable depth. A composite target is verified using a satisfiability solver, and in response to determining that the verifying step has hit the composite target, a counterexample to is examined to identify one or more reasons for the first target to be asserted. One or more refinement pairs are built by examining the counterexample, and a second abstraction is built by composing the refinement pairs. One or more learned clauses and one or more invariants to the second abstraction and the second abstraction is chosen as the current abstraction. The current abstraction is verified with the satisfiability solver.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.