通过突破符号快速错误检测边界实现处理器核的有效硅前验证
硬件体系结构
2021-07-01 v1 计算机科学中的逻辑
摘要
我们提出一种处理器设计硅前验证的新方法。硅前验证的目的是在早期阶段发现设计中的逻辑错误，从而避免耗时且昂贵的硅后调试。我们的方法依赖于符号快速错误检测（Symbolic QED，或 SQED）。SQED 结合有界模型检测（BMC）与 QED 测试，旨在符号化设计表示中发现逻辑错误。QED 测试擅长生成触发错误的短指令序列（迹）。我们用符号化起始状态扩展了已有的 SQED 方法。由此，我们使 BMC 工具在生成迹时可任意选择起始状态。为避免假阳性（例如，从不可达状态开始的迹可能不按处理器指令集架构行为），我们定义约束以限制可能的起始状态集合。我们证明这些约束连同对系统行为的合理假设，使我们能够避免假阳性。使用我们的方法，我们在开源 RISC-V 处理器核中发现了现有方法无法检测的未知错误。此外，我们的新方法在检测具有长迹的错误和检测硬件木马（即设计的未授权修改）方面优于现有方法。
引用
@article{arxiv.2106.10392,
title = {Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection},
author = {Karthik Ganesan and Florian Lonsing and Srinivasa Shashank Nuthakki and Eshan Singh and Mohammad Rahmani Fadiheh and Wolfgang Kunz and Dominik Stoffel and Clark Barrett and Subhasish Mitra},
journal= {arXiv preprint arXiv:2106.10392},
year = {2021}
}
备注
This article has the full author list which was missing in arXiv:1908.06757. arXiv admin note: substantial text overlap with arXiv:1908.06757