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

Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study” by E. Singh, K. Devarajegowda, S. Simon, R. Schnieder, K. Ganesan, M. Fadiheh, D. Stoffel, W. Kunz, C. Barrett, W. Ecker, and S. Mitra. In Proceedings of the 2019 Design, Automation and Test in Europe (DATE '19), Mar. 2019, pp. 1000-1005. Florence, Italy.

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.

BibTeX entry:

@inproceedings{SDS+19,
   author = {E. Singh and K. Devarajegowda and S. Simon and R. Schnieder
	and K. Ganesan and M. Fadiheh and D. Stoffel and W. Kunz and C.
	Barrett and W. Ecker and S. Mitra},
   title = {Symbolic {QED} Pre-silicon Verification for Automotive
	Microcontroller Cores: Industrial Case Study},
   booktitle = {Proceedings of the 2019 Design, Automation and Test in
	Europe (DATE '19)},
   pages = {1000--1005},
   publisher = {IEEE},
   month = mar,
   year = {2019},
   isbn = {978-3-9819263-2-3},
   doi = {10.23919/DATE.2019.8715271},
   note = {Florence, Italy},
   url = {http://theory.stanford.edu/~barrett/pubs/SDS+19.pdf}
}

(This webpage was created with bibtex2web.)