Assertion extraction from design and its signal traces
US9626468B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Feb 27, 2014 |
| Grant date | Apr 18, 2017 |
| Priority date | — |
| Expiry date | Mar 2, 2035 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/30
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Groups of signals in an electronic design for which interesting assertions, such as assert, assume and cover properties, can be generated are identified. A sliding temporal window of fixed depth is used to sample unique present and past value combinations of signals in the signals groups generated by one or more simulations or emulations. The values of signals in the signal groups are organized into truth tables. Minimal functional relations are extracted from the truth tables, using techniques similar to those for synthesis of partial finite memory machines from traces, and used to generate assertions. The assertions are filtered using a cost function and pertinence heuristics, and a formal verification tool used to prune unreachable properties and generate traces for reachable cover properties. Syntactically correct assert, assume and cover property statements for the generated properties are instantiated and packaged into a file suitable for further simulation or emulation or formal verification.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.