提升符号 QED 的边界以实现处理器核高效硅前验证
硬件体系结构
2021-06-18 v4 密码学与安全
计算机科学中的逻辑
摘要
现有在硅前验证中确保功能正确性与硬件可信的技术面临严重局限。本工作中，我们系统性地利用两个关键思想：1）符号快速错误检测（Symbolic QED 或 SQED），一种使用有界模型检测（BMC）的近期错误检测与定位技术；以及 2）符号起始状态，以提出一种方法：i）有效检测“困难”逻辑错误与硬件木马，即使在传统 BMC 技术失效的较长激活序列下；以及 ii）不需要熟练的手动指导来编写测试平台、编写设计专用断言或调试伪反例。使用开源 RISC-V 核，我们展示了如下结果：1. 对来自商用芯片与研究文献的数百个逻辑错误与硬件木马场景的 100% 快速检测（顺序标量核少于 5 分钟，乱序超标量核少于 2.5 小时），以及对“极端”错误（需要约 100,000 条取自随机测试程序的激活指令的随机生成错误）的 97.9% 检测。2. 对开源 RISC-V 设计中若干先前未知错误的快速（约 1 分钟）检测。
引用
@article{arxiv.1908.06757,
title = {Boosting the Bounds of Symbolic QED for Effective Pre-Silicon Verification of Processor Cores},
author = {Karthik Ganesan and Srinivasa Shashank Nuthakki},
journal= {arXiv preprint arXiv:1908.06757},
year = {2021}
}
备注
arXiv admin note: withdrawn by arXiv administrators due to incomplete author list