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

Eshan Singh, Keerthikumara Devarajegowda, Sebastian Simon, Ralf Schnieder, Karthik Ganesan, Mohammad Fadiheh, Dominik Stoffel, Wolfgang Kunz, Clark Barrett, Wolfgang Ecker, Subhasish Mitra

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

11 Scopus citations

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.

Original languageEnglish
Title of host publicationProceedings of the 2019 Design, Automation and Test in Europe Conference and Exhibition, DATE 2019
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1000-1005
Number of pages6
ISBN (Electronic)9783981926323
DOIs
StatePublished - 14 May 2019
Event22nd Design, Automation and Test in Europe Conference and Exhibition, DATE 2019 - Florence, Italy
Duration: 25 Mar 201929 Mar 2019

Publication series

NameProceedings of the 2019 Design, Automation and Test in Europe Conference and Exhibition, DATE 2019

Conference

Conference22nd Design, Automation and Test in Europe Conference and Exhibition, DATE 2019
Country/TerritoryItaly
CityFlorence
Period25/03/1929/03/19

Keywords

  • Bounded Model Checking
  • Formal verification
  • Presilicon verification
  • Symbolic Quick Error Detection

Fingerprint

Dive into the research topics of 'Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study'. Together they form a unique fingerprint.

Cite this