应用形式验证彻底验证RISC-V处理器设计。
不久前,许多半导体和系统供应商开发自己的处理器,针对特定的目标应用程序通常具有独特的特性。虽然这创新持续等专业处理器数字信号处理(DSP)引擎和图形处理单元(gpu),中央处理单元(cpu)很大程度上变成了一个two-contestant x86和ARM设计之间的比赛。最近,有兴趣增加高度定制的处理器的设计和验证。这部分是由于开放的性质和灵活性RISC-V标准,和一定程度上对处理器的要求人工智能(AI)、物联网(物联网),和其他先进的应用程序。
在OneSpin最近的渗透用户的小组会议在慕尼黑,我们的一个专家用户呈现一场精彩的应用形式验证彻底验证RISC-V处理器设计。Keerthi Devarajegowda是英飞凌科技研究员追求博士学位在你凯泽斯劳滕,德国。他发展了他的谈话“GapFree处理器验证由S²QED和财产的一代”英飞凌和TU凯泽斯劳滕的几个同事。他承认博士生默罕默德·r·Fadiheh是这种方法的主要贡献者之一。Keerthi开始讨论处理器使用模拟验证,错误可以逃到硅,和形式验证,传统上需要一个高水平的手动工作和正式的专业知识。他的主要研究兴趣是pre-silicon验证的属性生成的自动化,更容易地使用正式的和更有效的。
他分类逻辑错误处理器分为两类。单指令错误发生在当一个指令提供了错误的结果无论程序上下文,以前执行的指令序列。多个指令错误发生只有当的指令序列执行一个特定的顺序。例如,管道风险检测单位可能有一个错误,结果在一个指令接收寄存器的旧值之前早些时候已经更新的指令。单指令错误后可以检测到一个属性是每条指令书面和正式证明。为多个指令,很难想象所有可能的程序上下文和手动指定要证明所有属性。这一挑战的刺激他的研究在自动属性的一代。
Keerthi走前观众通过一系列技术用于验证英飞凌处理器的方法。他开始通过描述快速错误检测(QED) post-silicon处理器验证技术,仪器和各种转换和检查软件测试。每条指令序列测试转换使用不同的寄存器,并从原始和修改测试结果进行了比较。任何差异表明一个特定的序列相关的多个指令错误涉及多个寄存器。QED是有效地发现缺陷错误检测较短的延迟。
象征性的快速错误检测(平方)这个大意和移到pre-silicon使用形式验证方法验证。处理器设计装备为寄存器文件分割成两半,和正式的分析考虑所有可能的QED测试长度“k”,可以运行在两个部分。任何分歧(正式的反例)表示多个指令错误。如果没有发现bug,正式的引擎可以提供一个有界的正确性证明深度“k”所以缺陷仍可能被错过。因此,平方是有效的寻找多个指令错误而不是证明他们的缺席。获得完整的平方(无限)证明需要使用象征性的初始状态(S²QED)。
Keerthi解释说,S²QED正式考虑并行执行相同的测试在两个独立的处理器和相同的实例。假设一致的寄存器值和相同的两个实例之间的指令序列,一个正式的引擎可以证明两个寄存器集将在每个序列一致。与sqe,任何正式的分析揭示了一个反例发现多个指令错误。Keerthi然后提出的问题如何实现完整的处理器验证(c²QED),这样单指令验证,和用户知道属性完全覆盖所有处理器的行为。这可以通过生成一个S²QED属性为每个指令类+重置属性,并应用一组完整性检查。
Keerthi封闭的一个实际例子验证一个CPU使用c²QED的方法。设计是一个32位的英飞凌RISC-V处理器与整数指令,实现五级管道顺序获取和顺序提交。测量的复杂性,设计包含3472位状态。花了大约五engineer-days建立和运行形式验证,加上一个额外的一天一个新的指令扩展。正式运行发现设计缺陷的30秒内运行时。一旦所有的bug被发现,一个无界的正式证明了只有18分钟的运行时。仿真需要几周或几个月,当然,不可能已经证明没有bug。
所有的属性都自动生成使用英飞凌元建模框架。所有正式分析OneSpin 360DV-Certify解决方案,包括GapFreeVerification应用程序以确保设置生成的属性是完整的。Keerthi的结论是,这种高度自动化的正式技术处理器验证产生“非常好的提高验证效率。“我们想感谢他加入渗透和OneSpin分享这个创新使用的产品。他的完整的演示视频是可用的https://onespin.com/resources/videos/osmosis-2019/keerthi-devarajegowda-infineon-technologies。我们希望你跟我们一样喜欢它。
|
|
|
|
|
|
|
|
|
|
留下一个回复