RISC-V自定义拓展验证难？VC Formal给出全套解决方案

从拥抱趋势、畅想未来，到解决问题、交付产品，RISC-V 芯片已被广泛使用。据咨询机构 Semico Research 测算，截止 2024 年底全球 RISC-V 核的累积使用量已达 500 亿颗——地球上人均 6 颗。从“RISC-V 将无处不在”到“RISC-V，就现在”，RISC-V 已几乎覆盖所有应用。当前，RISC-V 已成功跻身世界主流处理器市场，不再局限于低功耗小设备，而是明确向智能汽车、工业、5G基站、端侧AI 乃至数据中心等高价值领域纵深推进。

RISC-V 远超常规的，独特的验证挑战

在半导体和系统设计中，验证的目标是证明我们计划构建的产品能够实现预期的各项功能，并且永远不会出现任何异常行为。智能化的今天，电子设备的复杂性正在迅速增加，对于错误的容忍度却在不断降低，存在缺陷的产品轻则导致召回，严重的甚至可能导致致命事故。因此对于芯片而言，从设计到交付，验证是过程中关键的一环，对于验证的要求也越来越高。

对于 RISC-V 来说，验证还有一些远超常规的，独特的验证挑战。

RISC-V 是指令集架构而不是芯片架构本身。RISC-V 指令集架构由一个精简的基础指令集和一系列可选的标准扩展组成，设计者可以像搭积木一样选择指令集。除此之外，设计者还可以添加专用指令完成自定义拓展，用来优化特定应用（如 AI 加速、加密、DSP 等）。当设计者使用 RISC-V ISA 进行架构设计时，首先就要进行 ISA（指令集架构）的合规性完备测试。

RISC-V 的开源、开放以及灵活性吸引了大量厂商和开源社区开发专属的微架构内核或者 IP 模块。这些微架构可以实现相同的基础 ISA 和标准扩展，但在控制路径和数据路径中，有许多实现选择。不同的选择，在性能、功耗和复杂性方面也可能存在差异，这导致了复杂的微架构验证需求，每一个不同的 RISC-V 微架构内核和 IP 都需要自己的微架构验证来验证处理器的内部实现细节。设计者的自定义拓展甚至可能显著改变处理器的行为（比如改变了流水线中的内容、ALU 中的冲突、缓存系统问题或者加载存储内容），每一项自定义拓展都会使验证难度加倍，添加的所有内容必须完全重新验证，不仅要保证功能正确，还要确保它们保持系统一致性。

形式化验证的优点

形式化验证的核心是通过数学证明，穷举所有可能的设计行为。经过多年的发展，现在形式化验证已经与仿真、硬件加速和硬件原型设计并驾齐驱，随着设计复杂度提高和验证难度提高，发展形式化验证已经势在必行。

形式化验证拥有许多优点：

在设计早期就能发现潜在的错误和漏洞，可以为设计团队节省大量时间和精力。

除了初始设置和 property 开发，验证过程大部分是全自动的。

RTL 一旦就绪就可以开始验证，适合敏捷过程。

发现 property 反例的速度比动态验证快得多。

值得信赖，形式化验证穷举所有可能，拥有 100% 确定性。

新思科技 VC Formal 解决方案在 RISC-V 验证中的应用

新思科技推出的新一代形式化验证解决方案 VC Formal 是业内领先的形式化验证工具，与 Synopsys VCS®、Verdi®、VC SpyGlass™、VC Z01X 故障模拟及其他新思科技设计与验证解决方案协同工作。VC Formal 拥有出色的容量、速度和灵活性，可验证某些最艰巨的设计挑战，比如关键模块的 bug-free 验证。VC formal 结合统一的 VCS 编译和 Verdi 调试可帮助用户减少迁移投入，快速调试遇到的问题，并通过支持 VCS UNR 解决方案实现更快的覆盖收敛。

VC Formal 解决方案包括一整套 APP：属性验证 (FPV)、自动提取属性 (AEP)、覆盖分析器 (FCA)、连接性检查 (CC)、时序等效性检查 (SEQ)、寄存器验证 (FRV)、测试平台分析仪 (FTA)、形式导航器 (Navigator) 以及用于验证标准总线协议的一组断言 IP (AIP）等。

VC Formal 解决方案可完美应用于 RICS-V 内核与 IP 模块的验证。在 RISC-V 内核与模块的验证中，所有能够通过 SVA 的方式描述出来的控制逻辑，都可以通过 FPV（属性断言验证）来做检查。针对运算逻辑，DPV（数据通路验证）主要提供 C model 和 RTL 的等价性检查。SEQ（等价性检查）可以保证 RTL 阶段引入门控时钟前后，两份 RTL 的功能一致性。寄存器验证（FRV）从形式上验证 RISC-V CSR 的行为，如 “只读”“读/写”“复位值” 等属性，无需再通过定向测试验证。FSV（安全检查）可以保证安全数据不会发生传播泄漏或者被篡改，保障数据完整性。

新思科技提供完整的、高性能、优化后的断言 IP 库，可用于验证标准总线协议如 AMBA 协议，兼容 VC Formal 形式化验证以及 VCS 仿真。用户可直接调用该 IP 库，无需从零构建断言 IP，大幅缩短验证启动时间。

其中，RISC-V ISA 断言 IP 可以用在 ISA（指令集架构）的合规性完备测试中。它可以形式化测试所有可能的 RISC-V 指令场景，验证指令执行控制路径和基本 ISA 数据路径，并可用于多种配置和内核。

结语

开放的 RISC-V 正在为计算产业带来创新活力，从设计到交付，完善的验证至关重要。新思科技在 RISC-V 验证领域处于领先地位，持续推动 RISC-V 技术标准化与工具链整合，为 RISC-V 产业落地提供了坚实支撑，携手全球开发者加速 RISC-V 的创新发展与生态繁荣。