Elimination of illegal states within equivalence checking
US9501597B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Jul 11, 2014 |
| Grant date | Nov 22, 2016 |
| Priority date | — |
| Expiry date | Jul 11, 2034 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/398
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method for equivalence checking includes obtaining a first and a second representation for a semiconductor design and applying a set of inputs to both representations. The outputs of the first representation are compared to the outputs of the second representation. If a mismatch is found, the starting states for the first and second representations are evaluated using a model checker to see if they are reachable from a known legal state such as reset state for that representation. If both of the starting states are reachable, the mismatch is a real mismatch providing a counter-example of the equivalence of the two representations. If one or both of the starting states are unreachable, the mismatch is a spurious mismatch and the model checker can be used to generate an invariant to preclude those starting states in future iterations of the equivalence checker.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.