Symbolic QED Pre-Silicon Verification for Automotive Microcontroller Cores: Industrial Case Study
Eshan Singh1, Keerthikumara Devarajegowda2,3, Sebastian Simon2, Ralf Schnieder2, Karthik Ganesan1, Mohammad Fadiheh3, Dominik Stoffel3, Wolfgang Kunz3, Clark Barrett1, Wolfgang Ecker2,4 and Subhasish Mitra1
1Stanford University, Stanford, CA, USA
2Infineon Technologies AG, Germany
3Technische Universitat Kaiserslautern, Germany
4Technische Universitat Miinchen, Germany
ABSTRACT
We present an industrial case study that demonstrates the practicality and effectiveness of Symbolic Quick Error Detection (Symbolic QED) in detecting logic design flaws (logic bugs) during pre-silicon verification. Our study focuses on several microcontroller core designs ((1,800 flip-flops, (70,000 logic gates) that have been extensively verified using an industrial verification flow and used for various commercial automotive products. The results of our study are as follows: 1. Symbolic QED detected all logic bugs in the designs that were detected by the industrial verification flow (which includes various flavors of simulation-based verification and formal verification). 2. Symbolic QED detected additional logic bugs that were not recorded as detected by the industrial verification flow. (These additional bugs were also perhaps detected by the industrial verification flow.) 3. Symbolic QED enables significant design productivity improvements: (a) 8X improved (i.e., reduced) verification effort for a new design (8 person-weeks for Symbolic QED vs. 17 person-months using the industrial verification flow). (b) 60X improved verification effort for subsequent designs (2 person-days for Symbolic QED vs. 4-7 person-months using the industrial verification flow). (c) Quick bug detection (runtime of 20 seconds or less), together with short counterexamples (10 or fewer instructions) for quick debug, using Symbolic QED.
Keywords: Bounded Model Checking, Formal verification, Pre-silicon verification, Symbolic Quick Error Detection
