Constructing inductive counterexamples in a multi-algorithm verification framework
US8589837B1 · kind B1 · utility
Assignee
Inventors
Key dates
| Filing date | Apr 25, 2012 |
| Grant date | Nov 19, 2013 |
| Priority date | — |
| Expiry date | Apr 25, 2032 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A computer-implemented method simplifies a netlist, verifies the simplified netlist using induction, and remaps resulting inductive counterexamples via inductive trace lifting within a multi-algorithm verification framework. The method includes: a processor deriving a first unreachable state information that can be utilized to simplify the netlist; performing a simplification of the netlist utilizing the first unreachable state information; determining whether the first unreachable state information can be inductively proved on an original version of the netlist; and in response to the first unreachable state information not being inductively provable on the original netlist: projecting the first unreachable state information to a minimal subset; and adding the projected unreachable state information as an invariant to further constrain a child induction process. Adding the projected state information as an invariant ensures that any resulting induction counterexamples can be mapped to valid induction counterexamples on the original netlist before undergoing the simplification.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.