Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study
Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study
复制标题
汽车微控制器内核的符号 QED 硅前验证：工业案例研究
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
S. Mitra
中科院分区：
文献类型：
--
作者：
Eshan Singh;Keerthikumara Devarajegowda;Sebastian Simon;Ralf Schnieder;K. Ganesan;M. R. Fadiheh;D. Stoffel;W. Kunz;Clark W. Barrett;W. Ecker;S. Mitra
我们提出了一个工业案例研究，证明了实用性和有效性的符号快速错误检测（符号QED）在检测逻辑设计缺陷（逻辑错误）在预硅验证。我们的研究重点是几个微控制器核心设计（约1，800个触发器，约70，000个逻辑门），这些设计已经使用工业验证流程进行了广泛验证，并用于各种商业汽车产品。我们的研究结果如下：1.符号QED检测到所有的逻辑错误的设计，被检测到的工业验证流程（包括各种口味的基于模拟的验证和形式验证）。2.符号QED检测到额外的逻辑错误，没有被记录为检测到的工业验证流程。（这些额外的错误也可能被工业验证流程检测到。3.符号QED能够显著提高设计生产率：（a）提高8倍（即，减少）验证工作量（符号QED为8人-周，而使用工业验证流程为17人-月）。（B）后续设计的验证工作量提高了60倍（符号QED为2人日，而使用工业验证流程为4-7人月）。（c）快速错误检测（运行时间为20秒或更短），以及使用符号QED的快速调试的短反例（10条或更少的指令）。
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.