Integrating Symbolic Simulation of C/C++ into a Comprehensive EDA Verification Environment
Tom Melham, Andreas Tiemeyer, Daniel Kröning, John W. O’Leary · 2023
Formal verification of chip designs - once thought to be an impractical dream - has matured through many years of technological innovation, investment, and experience into a mainstream verification tool used across the semiconductor design industry. Mature and highly capable tools, with rich debugging environments, are available from the EDA vendors - and the technology continues to advance. This talk will tell the story of how a software verification tool for C programs - the CMBC bounded model checker developed by Daniel Kroening - was leveraged to integrate C/C++ symbolic simulation into a commercial formal verification environment. The aim of this project was to move beyond an academic prototype and enable equivalence checking of digital circuit models against real-world C/C++ reference model code – with full access to the proof engines, verification control, and debugging tools of a leading commercial verification environment.