Method and system for performing utilization of traces for incremental refinement in coupling a structural overapproximation algorithm and a satisfiability solver
US7448005B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Jan 26, 2006 |
| Grant date | Nov 4, 2008 |
| Priority date | — |
| Expiry date | May 3, 2027 |
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. The method includes creating and designating as a current abstraction a first abstraction of an initial design netlist containing a first target and unfolding the current abstraction 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 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. A new target is built over one or more cutpoints in the first abstraction that is asserted when the one or more cutpoints assume values in the counterexample, and the new target is verified with the satisfiability solver.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.