Formal verification using cached search path information to verify previously proved/disproved properties
US10503853B1 · kind B1 · utility
Assignee
Inventors
Key dates
| Filing date | Jul 27, 2018 |
| Grant date | Dec 10, 2019 |
| Priority date | — |
| Expiry date | Jul 27, 2038 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/30
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A formal verification tool that verifies multiple sequentially-generated versions of a core circuit design by obtaining search path information from the formal verification solver for each property that is proven or disproven during a first formal verification session involving an earlier-generated circuit design version, and utilizing the search path information to perform search-path verification processes during a subsequent formal verification session to quickly verify the proven/disproven properties in a later-generated circuit design version. Each property's search path information includes counterexample traces or proof artifacts identifying the search operations utilized to achieve a corresponding counterexample or proof object that proves/disproves the property. Search-path verification involves applying the stored search path information to the later-generated circuit design version, and determining if the same counterexample or proof object is achieved. The stored search path information is also utilized to perform efficient path-influenced search processes when the search-path verification process fails.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.