Using runtime information from solvers to measure quality of formal verification
US10657307B1 · kind B1 · utility
Assignee
Inventors
Key dates
| Filing date | Jun 29, 2018 |
| Grant date | May 19, 2020 |
| Priority date | — |
| Expiry date | Aug 3, 2038 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/30
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Systems and techniques are described for using runtime information to identify a verification hole and/or compute a verification metric. Runtime information (RI) for a set of proven assertions can be determined, wherein the RI includes a first set of registers, a first set of inputs, and a first set of constraints that were used by a formal verification engine during runtime to prove one or more assertions for a design under verification (DUV). Next, a second set of registers, a second set of inputs, and a second set of constraints that are not present in the RI can be determined. The second set of registers, the second set of inputs, and/or the second set of constraints can then be used to (1) identify a verification hole and/or (2) compute a verification metric.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.