REVERSE: Efficient Sequential Verification for Retiming
Maher N. Mneimneh, Karem A. Sakallah · 2003
a new framework for verifying the sequential equiva- lence of circuits optimized by retiming. Our approach recognizes the existence of a retiming invariant relating the two circuits, and utilizes that invariant in an induction-based verification paradigm. We prove useful properties about that invariant and present efficient algorithms for computing as well as employing it for verification. We demonstrate encouraging results on the ISCAS 89 benchmarks.