Semi-Formal Verification at IBM

Summary form only given. This talk focuses on the IBM internal (semi-)formal verification toolset SixthSense. We first provide a high-level overview of the SixthSense tool, developed to perform functional verification as well as sequential equivalence checking. We introduce the various synergistic transformation and verification engines it encompasses, encapsulated within a novel transformation-based verification framework. We have found this algorithmic synergy critical to enabling core semi-formal search algorithms to identify the most complex and deep bugs, as well as to enabling the completion of difficult correctness proofs. We additionally discuss various industrial applications of this toolset, from lighter-weight assertion and constraint-based verification to comprehensive block or unit-level reference model style of verification to silicon-failure recreation efforts