TY - GEN
T1 - Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores
T2 - 22nd Design, Automation and Test in Europe Conference and Exhibition, DATE 2019
AU - Singh, Eshan
AU - Devarajegowda, Keerthikumara
AU - Simon, Sebastian
AU - Schnieder, Ralf
AU - Ganesan, Karthik
AU - Fadiheh, Mohammad
AU - Stoffel, Dominik
AU - Kunz, Wolfgang
AU - Barrett, Clark
AU - Ecker, Wolfgang
AU - Mitra, Subhasish
N1 - Publisher Copyright:
© 2019 EDAA.
PY - 2019/5/14
Y1 - 2019/5/14
N2 - 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.
AB - 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.
KW - Bounded Model Checking
KW - Formal verification
KW - Presilicon verification
KW - Symbolic Quick Error Detection
UR - http://www.scopus.com/inward/record.url?scp=85066633170&partnerID=8YFLogxK
U2 - 10.23919/DATE.2019.8715271
DO - 10.23919/DATE.2019.8715271
M3 - Conference contribution
AN - SCOPUS:85066633170
T3 - Proceedings of the 2019 Design, Automation and Test in Europe Conference and Exhibition, DATE 2019
SP - 1000
EP - 1005
BT - Proceedings of the 2019 Design, Automation and Test in Europe Conference and Exhibition, DATE 2019
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 25 March 2019 through 29 March 2019
ER -