Logic design verification techniques for liveness checking with retiming

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.