Patent Document ID: 8255848
Application ID: 12394560
Patent Flag: 1

Claim One:
1. A method for verification of a retimed integrated circuit logic design using liveness checking as set forth by instructions executed by a computer system, comprising: assigning, by one or more instructions executed by the computer system, a liveness gate to a liveness property for an original netlist; assigning, by one or more instructions executed by the computer system, a fairness gate to a fairness constraint for the original netlist, where 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; retiming by one or more instructions executed by the computer system, using a retiming engine, the original netlist to provide a retimed netlist, wherein 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; performing, by one or more instructions executed by the computer system, verification analysis on the retimed netlist; returning as an output of the computer system, when the verification analysis yields a valid counter-example trace for the retimed netlist, a liveness violation for the original netlist; and mapping, by one or more instructions executed by the computer system, the valid counter-example trace obtained for the retimed netlist to the original netlist to provide a mapped counter-example trace for the original netlist, wherein the liveness and fairness gates of the retimed netlist are retimed by a first lag and the mapping further includes: delaying, by one or more instructions executed by the computer system, a loop signal, provided by a single loop gate, in the retimed netlist by the first lag to determine an assertion of the loop signal in the mapped counter-example trace; and truncating, by one or more instructions executed by the computer system, a length of the mapped counter-example trace to provide a resulting counter-example trace .