Logic design verification techniques for liveness checking with retiming
US8255848B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Feb 27, 2009 |
| Grant date | Aug 28, 2012 |
| Priority date | — |
| Expiry date | Dec 5, 2030 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F2119/12
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A technique for verification of a retimed logic design using liveness checking includes assigning a liveness gate to a liveness property for an original netlist and assigning a fairness gate to a fairness constraint for the original netlist. In this case, the fairness gate is associated with the liveness gate and is asserted for at least one time-step during any valid behavioral loop associated with the liveness gate. The original netlist is retimed, using a retiming engine, to provide a retimed netlist. The liveness and fairness gates of the retimed netlist are retimed such that a lag of the fairness gate is no greater than a lag of the liveness gate. Verification analysis is then performed on the retimed netlist. Finally, when the verification analysis yields a valid counter-example trace for the retimed netlist, a liveness violation for the original netlist is returned.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.