System, method, and computer program product for sequential equivalence checking in formal verification
US10984161B1 · kind B1 · utility
Assignee
Inventors
Key dates
| Filing date | Nov 20, 2019 |
| Grant date | Apr 20, 2021 |
| Priority date | — |
| Expiry date | Nov 20, 2039 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F2119/16
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
The present disclosure relates to a computer-implemented method for use in a formal verification of an electronic design. Embodiments may include receiving a reference model including a software specification, an implementation model at a register transfer level, and a property that analyzes equivalence between the reference model and the implementation model. The method may further include generating one or more case split hints based upon the reference model, that may be used to decompose the design state space into smaller partitions and performing an abstraction operation on a portion of design logic associated with one or more partitions in order to eliminate design elements that are irrelevant to a particular property. Embodiments may also include performing model checking on the abstract models to determine their accuracy.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.