利用先进形式验证工具来高效完成RISC－V处理器验证

作者：Laurent Arditi, Paul Sargent, Thomas Aird
职务：Codasip高级验证/形式验证工程师

我们在上一篇技术白皮书《基于形式验证的高效RISC-V处理器验证方法》中，以Codasip L31这款用于微控制器应用的32位中端嵌入式RISC-V处理器内核为例，介绍了一个基于形式验证的、易于调动的RISC-V处理器验证程序。它与RISC-V ISA黄金模型和RISC-V合规性自动生成的检查一起，展示了如何有效地定位那些无法进行仿真的漏洞。

RISC-V的开放性允许定制和扩展基于RISC-V内核的架构和微架构，以满足特定需求。这种对设计自由的渴望也正在将验证部分的职责转移到不断壮大的开发人员社群。然而，随着越来越多的企业和开发人员转型RISC-V，大家才发现处理器验证绝非易事。新标准由于其新颖和灵活性而带来的新功能会在无意中产生规范和设计漏洞，因此处理器验证是处理器开发过程中一项非常重要的环节。

在复杂性一般的RISC-V处理器内核的开发过程中，会发现数百甚至数千个漏洞。当引入更多高级特性的时候，也会引入复杂程度各不相同的新漏洞。而某些类型的漏洞过于复杂，导致在仿真环节都无法找到它们。因此必须通过添加形式验证来赋能RTL验证方法。从极端漏洞到隐匿式漏洞，形式验证能够让您在合理的处理时间内详尽地探索所有状态。

在本文中，我们将以西门子EDA处理器验证应用程序为例，结合Codasip L31这款广受欢迎的RISC-V处理器IP提供的特性，来介绍一种利用先进的EDA工具，在实际设计工作中对处理器进行验证的具体方法。这种验证方法通过为每条指令提供一组专用的断言模板来实现高度自动化，不再需要手动设计，从而提高了形式验证团队的工作效率。

如何使用西门子EDA处理器验证应用程序

在我们使用该工具之前，需要为Codasip L31 RISC-V内核进行形式验证设置。此设置类似于使用带有抽象、约束等基于断言的验证（ABV）方法来形式验证标准断言的设置。

该工具允许验证特定类别的指令，并启用或禁用某些资源检查。有了这个工具，我们的验证可以从一个简化的空间开始，这包括：

• 只有最简单的指令，例如只有整数运算和逻辑指令。
• 只有最简单（但最重要）的检查。例如通用寄存器的更新。稍后可以添加的其他检查指的是系统寄存器（CSR）或程序计数器（PC）的更新以及内存访问。
• 只有主功能模式：没有中断、中止、异常或调试访问。

这三个正交约束可以根据微架构特征的关键程度逐一放宽。经典的形式验证技术可用于帮助获得检查器断言的结果：抽象、设计缩减、案例拆分、不变量生成、半形式漏洞搜寻等。

结果

这种基于形式的方法使我们能够找到极端情况，并深入了解改进我们的仿真和测试平台。在其他基于仿真的验证流程运行而未发现新漏洞之后，此验证工作在项目快结束时完成，这使我们能够找到真正的和重要的漏洞。

我们可以特别关注其中的三个漏洞，它们从用于L31的西门子EDA处理器验证应用程序中找到。以下是发现和弥补这三个漏洞的具体方法：

1. 分支预测器损坏

有了这个漏洞，返回到先前持有跳转/分支指令的PC地址会导致分支预测器错误地预测跳转到另一个地址。当满足以下条件时，会发现这种极端情况：

自修改代码

当添加未定义的指令（新指令异常）时，也会出现此漏洞极其罕见的版本：

该漏洞是通过检查PC值的断言发现的，直接后果是错误地执行了一个分支指令，导致代码执行错误。通过正确清除分支预测和流水线的缓冲数据来修复此漏洞。

使用西门子EDA处理器验证应用程序查找此漏洞需要8个周期和15分钟的运行时间。在仿真中重现该漏洞需要一个支持自修改代码的随机生成器，该代码可正好返回相同的地址并将该地址从分支修改为另一种类型的指令。换句话说，随机生成器不可能做到这一点。只有知道漏洞详细信息的定向序列可以做到。

2. 同一条指令的多次执行

出现这个漏洞，NPC（下一个 PC）单元停顿就会出现，这会导致多次获取相同的地址。每条指令执行并退出。

当满足以下条件时，会出现这种极端情况：

• 内核配置有TCM。
• 在提取总线上可以看到特定的延迟。
• 在流水线内可以看到特定的停顿。

该漏洞会直接在流水线的其余部分造成未被正确处理的停顿，导致同一指令的多次执行。可以通过正确处理其余流水线中的停顿来修复此漏洞。

使用西门子EDA处理器验证应用程序查找此漏洞需要5个周期和10分钟的运行时间。在仿真中再现它需要随机延迟和停顿的随机模式，但也需要相当多的“运气”来再现这个特定序列。

3. 合法的 FENCE.I 指令被认为是非法的

出现这个漏洞，内存屏障会由CSR单元处理。如果与CSR操作的CSR地址位元对应的指令位元（位 [31:20]）与某些CSR寄存器（例如调试、计数器）匹配，则指令可能会被错误地标记为非法。

当满足以下条件时，会发现这种极端情况：

• imm[11:0]/rs1/rd 中有随机位元。
• 这些位元与其他一些非法指令相匹配。

该漏洞的直接后果是错误地引发了非法指令异常。通过正确解码流水线每个部分的完整指令可修复此漏洞。

使用西门子EDA处理器验证应用程序查找此漏洞仅用了8个周期和5分钟的运行时间。因为编译器只会创建最简单的二进制编码实现，所以很难在仿真中重现该漏洞。它需要一个特殊的编译器来创建合法编码的变体，或者使用各种编码进行特殊的定向测试。

从中发现的优势/结论

应用这种方法可以提高验证团队的工作效率。在项目的关键阶段提高效率。虽然在开始时构建正确的设置需要付出努力，但随着我们添加新的指令类别和新的检查器，进度就会加快。这个“最佳点”是我们发现大多数问题的地方，随着放宽约束以允许该工具探索更深奥的操作模式，速度就开始放缓。

图 1 验证L31 RISC-V内核的最佳效率的最佳点（来源：Codasip）

总的来说，因为使用西门子EDA处理器验证应用程序验证整个CPU所需的总体工作量远低于手动达到类似验证质量所需的工作量，所以使用该工具是相当高效的。在总共30个漏洞中，有15个是通过形式验证发现的。

表1  仿真 vs形式验证

当结合在一起到达高质量水平时，仿真和形式验证是非常强大的，并使我们能够促进改进验证的良性循环。

图 2 通过持续改进达到一流的品质（来源：Codasip）

该解决方案在Codasip L31这种3级流水线微控制器上的实施被证明是可行的，现在已部署到Codasip的下一代RISC-V内核中，包括嵌入式和应用内核。借助在L31上使用西门子EDA处理器验证应用程序积累的知识，即使应用内核更复杂，也可以减少建立稳健环境所需的工作量。而Codasip的下一步计划包括进一步研究该工具如何应用于超标量和乱序内核，以及支持新的 RISC-V 扩展。

补充阅读

RISC-V处理器的高效验证——技术白皮书：https://codasip.com/papers/efficientverification-of-riscv-processors-technical-paper/

构建用于处理器验证的瑞士奶酪模型方法 - 博客文章：https://codasip.com/2022/04/29/building-a-swiss-cheese-model-approach-for-processorverification/

本文摘录于《基于形式的高效 RISC-V 处理器验证方法 – 形式化验证》白皮书，出版人为总部位于欧洲的全球领先RISC-V供应商和处理器解决方案领导者，该公司的处理器IP目前已部署在数十亿颗芯片中。Codasip通过开放的RISC-V ISA、Codasip Studio处理器设计自动化工具与高品质的处理器IP相结合，为客户提供定制计算。这种创新方法能够轻松实现定制和差异化设计，从而开发出高性能的、改变游戏规则的产品，实现真正意义上的转型。如希望得到该白皮书的完整版本，可浏览Codasip中文网站或者关注该公司微信公众号。

该技术白皮书英文版下载链接：https://codasip.com/papers/a-formal-based-approach-for-efficient-riscv-processor-verification