Jason Baumgartner, Tamir Heyman, et al.
Formal Methods in System Design
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. © 2006 IEEE.
Jason Baumgartner, Tamir Heyman, et al.
Formal Methods in System Design
Krishnan Kailas, Viresh Paruthi, et al.
FMCAD 2009
Pradeep Kumar Nalla, Raj Kumar Gajavelly, et al.
ICCAD 2016
Gadiel Auerbach, Fady Copty, et al.
FMCAD 2010