Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study

TL;DR

This paper demonstrates that Symbolic QED is an effective and efficient pre-silicon verification method for automotive microcontroller cores, detecting all known bugs and significantly reducing verification effort.

Contribution

The study provides industrial evidence that Symbolic QED can detect all bugs found by traditional methods and offers substantial productivity improvements in automotive microcontroller verification.

Findings

Detected all bugs identified by industrial verification flow

Found additional bugs not recorded by traditional methods

Achieved up to 60X reduction in verification effort

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.