通过打破符号快速误错探测的界口,对处理核心进行有效的硅前有效核查 (Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection)

Karthik Ganesan,Florian Lonsing,Srinivasa Shashank Nuthakki,Eshan Singh,Mohammad Rahmani Fadiheh,Wolfgang Kunz,Dominik Stoffel,Clark Barrett,Subhasish Mitra

from arxiv, arXiv admin note: substantial text overlap with arXiv:1908.06757

We present a novel approach to pre-silicon verification of processor designs. The purpose of pre-silicon verification is to find logic bugs in a design at an early stage and thus avoid time- and cost-intensive post-silicon debugging. Our approach relies on symbolic quick error detection (Symbolic QED, or SQED). SQED is targeted at finding logic bugs in a symbolic representation of a design by combining bounded model checking (BMC) with QED tests. QED tests are powerful in generating short sequences of instructions (traces) that trigger bugs. We extend an existing SQED approach with symbolic starting states. This way, we enable the BMC tool to select starting states arbitrarily when generating a trace. To avoid false positives, (e.g., traces starting in unreachable states that may not be-have in accordance with the processor instruction-set architecture), we define constraints to restrict the set of possible starting states. We demonstrate that these constraints, togeth-er with reasonable assumptions about the system behavior, allow us to avoid false positives. Using our approach, we discovered previously unknown bugs in open-source RISC-V processor cores that existing methods cannot detect. Moreover, our novel approach out-performs existing ones in the detection of bugs having long traces and in the detection of hardware Trojans, i.e., unauthorized modifications of a design.

翻译：我们提出了对处理器设计进行硅前核查的新办法。硅前核查的目的是早期发现设计中的逻辑错误, 从而避免时间和成本密集的硅后调试。我们的方法依赖于象征性的快速错误探测( Symplic QED 或 SQED ) 。 SQED 的目标是通过将受约束的模型检查( BMC) 与 QED 测试结合, 以象征性的方式在设计中找到逻辑错误。 QED 测试在生成触发错误的短指令序列( traces) 方面是强大的。我们扩展了现有的SQED 方法, 从而避免了具有象征意义的启动状态的 SQED 方法。这样, 我们让 BMC 工具在生成跟踪时可以任意选择起始国。为了避免错误的正面效果, (例如, 开始在无法按照进程指令设置的结构进行接触的不可接触的国家中), 我们定义了限制可能的起始状态的调整的制约。我们证明这些制约, 在系统行为上的合理假设中, 使得我们能够避免有错误的错误的检测, ; 使用我们现有的核心的RIS 方法。