A formal-based approach for efficient RISC-V processor verification

Laurent Arditi, Paul Sargent, Thomas Aird (Codasip)

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

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

在本文中，我们将介绍一个基于形式验证的、易于调动的 RISC-V 处理器验证程序。与 RISC-V ISA 黄金模型和 RISC-V 合规性自动生成的检查一起，展示了如何有效地定位那些无法进行仿真的漏洞。通过为每条指令提供一组专用的断言模板来实现高度自动化，不再需要手动设计，从而提高了形式验证团队的工作效率。

1、基于先进内核的处理器开发

嵌入式系统的应用越来越广泛，同时对处理器的性能、功耗和面积（PPA）要求越来越高，因此我们将这样的产业和技术背景下用实际案例来分析处理器的验证。Codasip L31 是一款用于微控制器应用的 32 位中端嵌入式 RISC-V 处理器内核。作为一款多功能、低功耗、通用型的 CPU，它实现了性能和功耗的理想平衡。从物联网设备到工业和汽车控制，或作为大型系统中的深度嵌入式内核，L31可在一个非常小巧紧凑的硅片面积中实现本地处理能力。L31是通过 Codasip Studio 使用 CodAL 语言设计而成，该内核完全可定制，包括经典的扩展和特性，以及实现这些扩展和特性所需的高效和彻底的验证。

图1 Codasip L31处理器内核架构图解（来源：Codasip）

表 1 Codasip L31内核展示了RISC-V处理器的优异特性

2- 创建最优的RISC-V处理器验证方法

处理器验证需要制定合适的策略、勤勉的工作流程和完整性，而方兴未艾的、更加灵活的RISC-V处理器开发则需要针对自己处理器功能设置做详尽的验证规划；也需要参考一些内核供应商的内外部因素，比如该供应商自己的开发工具体现和外部开发工具伙伴，以及同系、同款或者同厂内核的出货量等。

验证处理器意味着需要考虑诸多不确定性。最终产品将运行什么软件？用例是什么？可能发生哪些异步事件？这些未知数意味着较大的验证范围。然而，覆盖整个处理器状态空间是无法实现的，这也不是Codasip这样的领先内核供应商的目标。

在确保处理器品质的同时，充分利用时间和资源才是处理器验证的正解。明智的处理器验证意味着在产品开发过程中尽早并高效地发现相关漏洞。在顶层方面，Codasip提供了多种创新的验证路径，其验证方法基于以下内容：

• 验证是在处理器开发期间与设计团队合作完成的。
• 验证是所有行业标准技术的组合。使用多种技术可以让您最大限度地发挥每一种技术的潜力，并有效地覆盖尽可能多的极端情况。
• 验证需持续进行。有效的办法是运用随着处理器复杂程度而不断发展的技术组合。

在验证L31内核时，我们的想法是让仿真和形式验证相辅相成。

2.1- 仿真的优势和目的

仿真实际上不可或缺，它允许我们在两个级别上进行验证设计：

• 顶层仿真（Top-level），主要是为了确保设计在最常见的情况下符合其规范（CPU 的 ISA）。
• 块级仿真（Block-level），以确保微架构按照预期设计。然而，很难将这些检查与顶层架构规范联系起来，因为这通常依赖于定向随机测试生成，因此能够应付棘手和不寻常的情况。

顶层仿真通常不像块级仿真那样特意强调设计。因此，它可以实现针对 ISA 的设计的整体验证。

2.2- 形式验证的优势和目的

形式验证使用数学技术对以断言形式编写的问题提供有关设计的明确答案。

形式验证工具对断言和设计的组合进行详尽的分析。不需要指定任何刺激，除了指定一些非正常情况以避免假漏洞。该验证工具可以提供详尽的“已证实”答案或“失败”答案，同时生成显示刺激的波形，证明断言是错误的。在大型和复杂的设计中，工具有时只能提供有限的证明，这意味着从重置到特定数量的周期都不存在漏洞场景。同时也存在不同的技术方法来增加该周期循环次数，或获得“已证明”或“失败”的答案。

形式验证用于以下情况：

• 为完整的验证一个模块，潜在地消除了任何仿真的需要。由于形式验证的计算复杂性，形式化验收（sign-off）仅限于小模块。
• 除了仿真之外，还要验证一个模块，即使是个大模块，因为形式验证能够在极端情况下找到漏洞，而随机仿真只能“靠运气”找到，而且概率非常低。
• 处理一些仿真不充分的验证任务，例如时钟门控、X态传播（X-propagation）、数据增量处理（CDC）、等价性检查等。
• 帮助调查缺少调试信息的已知漏洞，并确定潜在的设计修复。
• 对漏洞进行分类和识别，以便通过形式验证来学习和改进测试平台/仿真。
• 为了潜在地帮助仿真，填充覆盖范围中的漏洞。

3- 解决方案：一种基于形式验证的高效的 RISC-V 处理器验证方法

为了获得一种高效的RISC-V处理器验证方法，我们决定以采用西门子EDA 处理器验证APP来高效验证Codasip L31 RISC-V 内核为例，来进行详尽的说明。该工具的目标是确保 RTL 级别的处理器设计正确且详尽地实现指令集架构 （ISA）规范，而本文希望介绍的是一种端到端的解决方案

1- 该工具从一个顶层并有效的“黄金模型”中生成以下：

• 在 Verilog 语言中，ISA 的单周期执行模型。
• 一组断言，用于检查待测试模块 （DUT）和模型 （M）在架构级别的功能是否相同。

注意：这并没有进行任何正式等价性检查。

2- 当在 DUT 中获取新指令 （I）时，会捕获架构状态 （DUT-init）。

3- 该指令在流水线中运行。

4- 捕获另一个架构状态（DUT-final）。

5- M 被输入 DUT-init 和 I，并计算出一个新的 M-final 状态。

6- 断言检查 M-final 和 DUT-final 中的资源是否具有相同的值。

图 2 3 级 L31 内核的端到端验证流程（当验证指令 I 既没有停止也没有清除缓存数据时）

这种端到端的验证方法可以在比整个CPU 更小、更简单的模块（例如数据缓存）上合理实现。可以在缓存上写入端到端断言，以验证写入特定地址的数据是否从同一地址正确读取。这使用了众所周知的形式验证技术，例如记分牌算法。

然而，对于 CPU来说，手动编写这样的断言是不可行的。它需要指定每条指令的语义，并与所有执行模式交叉。这通常根本不可能实现。 CPU 的形式验证被分成更小的部分，但是仍然无法验证所有部分是否正确执行了 ISA。

使用建议的方法意味着能够立即验证完整的 L31 内核，而无需编写任何复杂的断言。如上所述，黄金模型和检查断言是自动生成的。

这种方法同时具有高度可配置性和自动化性，特别是对于 RISC-V CPU，例如 L31：

• 用户可以指定设计执行的顶层 RISC-V 参数和扩展。
• 该工具能够自动从设计中提取数据，例如将架构寄存器与实际每秒浮点运算次数相关联。
• 该工具允许添加自定义，例如用来验证的新指令（具有为用户“扩展”黄金模型的能力）。

最后，黄金模型不是由Codasip开发的（除了一些自定义部分），这一事实提供了额外的保证，这从验证独立性的角度来看很重要。

本文摘录于《基于形式的高效 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