Logic design verification techniques for liveness checking with retiming

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 .

2. The method of claim 1 , further comprising:

relabeling, by one or more instructions executed by the computer system, the liveness and fairness gates for the original netlist as a single super gate prior to retiming of the original netlist to ensure an equivalent lag between all the liveness and fairness gates.

3. The method of claim 1 , wherein the first lag corresponds to a maximum lag experienced by either of the liveness or fairness gates.

4. The method of claim 1 , wherein the first lag corresponds to a minimum lag experienced by either of the liveness or fairness gates.

5. The method of claim 1 , further comprising:

returning by one or more instructions executed by the computer system, when the verification analysis indicates a proof of correctness for the retimed netlist, a proof of correctness for the original netlist.

6. A computer-readable storage medium including code for verification of a retimed logic design using liveness checking, wherein the code, when executed, is configured to:

assign a liveness gate to a liveness property for an original netlist;

assign 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;

retime, 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;

perform verification analysis on the retimed netlist;

return, when the verification analysis yields a valid counter-example trace for the retimed netlist, a liveness violation for the original netlist, wherein the computer-readable storage medium is a tangible computer-readable storage medium; and

map 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 map code is further configured to:

delay 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

truncate a length of the mapped counter-example trace to provide a resulting counter-example trace.

7. The computer-readable storage medium of claim 6 , wherein the code, when executed, is further configured to:

relabel the liveness and fairness gates for the original netlist as a single super gate prior to retiming of the original netlist to ensure an equivalent lag between all the liveness and fairness gates.

8. The computer-readable storage medium of claim 6 , wherein the first lag corresponds to a maximum lag experienced by either of the liveness or fairness gates.

9. The computer-readable storage medium of claim 6 , wherein the first lag corresponds to a minimum lag experienced by either of the liveness or fairness gates.

10. The computer-readable storage medium of claim 6 , wherein the code, when executed, is further configured to:

return, when the verification analysis indicates a proof of correctness for the retimed netlist, a proof of correctness for the original netlist.

11. A computer system configured to verify a retimed logic design using liveness checking, comprising:

a memory subsystem for storing code; and

a processor coupled to the memory subsystem, wherein the processor is configured to execute code to:

assign a liveness gate to a liveness property for an original netlist;

assign 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;

retime, 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;

perform verification analysis on the retimed netlist;

return, when the verification analysis yields a valid counter-example trace for the retimed netlist, a liveness violation for the original netlist; and

map 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 map code is further configured to:

delay 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

truncate a length of the mapped counter-example trace to provide a resulting counter-example trace.

12. The computer system of claim 11 , wherein the processor is further is configured to execute code to:

relabel the liveness and fairness gates for the original netlist as a single super gate prior to retiming of the original netlist to ensure an equivalent lag between all the liveness and fairness gates.

13. The computer system of claim 11 , wherein the processor is further is configured to execute code to:

return, when the verification analysis indicates a proof of correctness for the retimed netlist, a proof of correctness for the original netlist.