汽车微控制器内核的符号 QED 硅前验证：工业案例研究
计算机科学中的逻辑
2019-10-16 v1
摘要
我们提出了一项工业案例研究，证明了符号快速错误检测(Symbolic QED)在硅前验证中检测逻辑设计缺陷（逻辑错误）的实用性与有效性。我们的研究聚焦于几个微控制器内核设计（约 1,800 个触发器，约 70,000 个逻辑门），这些设计已使用工业验证流程广泛验证并用于各种商用汽车产品。我们的研究结果如下：1. 符号 QED 检测到了工业验证流程（包括各种基于仿真的验证和形式化验证）检测到的设计中的所有逻辑错误。2. 符号 QED 检测到了工业验证流程未记录为已检测到的额外逻辑错误。（这些额外错误或许也被工业验证流程检测到了。）3. 符号 QED 实现了显著的设计生产力提升：(a) 新设计的验证工作量改进（即减少）8 倍（符号 QED 为 8 人周，而工业验证流程为 17 人月）。(b) 后续设计的验证工作量改进 60 倍（符号 QED 为 2 人天，而工业验证流程为 4—7 人月）。(c) 使用符号 QED 快速错误检测（20 秒或更少运行时间），以及用于快速调试的短反例（10 条或更少指令）。
引用
@article{arxiv.1902.01494,
title = {Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study},
author = {Eshan Singh and Keerthikumara Devarajegowda and Sebastian Simon and Ralf Schnieder and Karthik Ganesan and Mohammad R. Fadiheh and Dominik Stoffel and Wolfgang Kunz and Clark Barrett and Wolfgang Ecker and Subhasish Mitra},
journal= {arXiv preprint arXiv:1902.01494},
year = {2019}
}