Scalable conditional equivalence checking: An automated invariant-generation based approach

—Sequential equivalence checking (SEC) technologies, capable of demonstrating the behavioral equivalence of two designs, have grown dramatically in capacity over the past decades. The ability to efficiently identify and leverage internal equivalence points to reduce the domain of the overall SEC problem is central to SEC scalability. However, conditionally equivalent designs – within which internal equivalence may not exist under sequential observability don’t care conditions – are notoriously difficult for automated SEC tools. This paper constitutes one of the first attempts to advance the scalability of SEC for conditionally equivalent designs through automated invariant generation, which enables an inductive solution to an otherwise highlynoninductive problem. Through careful software engineering and various heuristics, this technique has been demonstrated capable of yielding orders of magnitude speedup on difficult industrial conditional SEC problems, in cases constitut...

• Type: Conference
• Year: 2009
• Where: FMCAD
• Authors: Jason Baumgartner, Hari Mony, Michael L. Case, Jun Sawada, Karen Yorav
• Keywords: FMCAD 2009, Formal Methods, Internal Equivalence, Overall Sec Problem, Sec Problems