Scalable Sequential Equivalence Checking across Arbitrary Design Transformations

High-end hardware design flows mandate a variety of sequential transformations to address needs such as performance, power, post-silicon debug and test. Industrial demand for robust sequential equivalence checking (SEC) solutions is thus becoming increasingly prevalent. In this paper, we discuss the role of SEC within IBM. We motivate the need for a highly-automated scalable solution, which is robust against a variety of design transformations - including those that alter initialization sequences. This motivation has caused us to embrace the paradigm of SEC with respect to designated initial states. We furthermore describe the diverse set of algorithms comprised within our SEC framework, which we have found necessary for the automated solution of the most complex SEC problems. Finally, we provide several experiments illustrating the necessity of our diverse algorithm flow to efficiently solve difficult SEC problems involving a variety of design transformations.