如何利用形式化验证提高RISC-V处理器质量？

在设计开发RISC-V处理器的过程中，通常遇到很多问题。以一个中等复杂程度的处理器为例，可以轻易浮现成百上千的错误漏洞。当在引入更多的高级功能时，漏洞也会不经意地被带入，这些漏洞复杂性各不相同。某些类型的漏洞太过于复杂，以致仿真无法发现它们，因此必须增强RTL验证方式方法。而增加形式验证是正解之一。从隐藏的案例到隐藏式漏洞，形式验证允许在合理的处理时间内详尽地探索状态。那么如何利用形式化验证来提高RISC-V处理器的质量？

为什么针对RISC-V使用形式化验证？

RISC-V是一个模块化的指令集架构，可以为其开发一个架构测试套件。它被用于基于仿真的验证，以验证一个处理器的实现。同样地，形式化方法可以用来验证处理器的架构符合性。为什么？因为RISC-V是一个开放的标准，每个人都可以把它作为一个参考模型来正式验证一个实现。

了解何时以及如何使用形式验证？

对于所有的硬件设计来说，形式化验证有好有坏，也有应用的好时机和坏时机。RISC-V处理器也不例外。

在项目开发的早期，有时甚至在仿真测试平台准备好之前，使用形式化是一个很好的方法，可以冲掉明显的错误漏洞。它可以确保以后执行的仿真步骤不会被这些bug所阻挡。另一方面，形式化验证在项目后期是非常有价值的，可以发现所有其他验证方法所遗漏的不易发现的错误。

形式化验证的不同变体的考虑主要有： 

基于断言的验证（ABV）- 使用低级断言。

使用高级断言的端到端验证，通常需要一个抽象的设计模型。

基于自动生成的断言的形式化流程也非常有用，如验证时钟门控的顺序等价检查，或X-传播验证。

当然更高级的验证技术也是适用的，这取决于模块的特性。例如，安全和功能安全应用。

除了这些，RISC-V处理器还可以用RISC-V ISA的架构模型进行端到端的验证。不过，应用这样的技术不能太早，因为大多数模块必须准备好并相互连接：指令获取、解码器、执行单元、加载-存储接口。可能不存在的模块或者因为不够成熟而被黑箱化的模块，y也可能包括内存管理单元（MMU）和缓冲器d等。

形式验证是瑞士奶酪模型验证方法的一个重要 "切片”。

Codasip的处理器验证方法依靠的是瑞士奶酪模型。通过这种方法，一些冗余是可以接受的，甚至是有针对性的。

冗余的重要性！

应用端到端的形式化方法，在内核上运行的仿真测试平台似乎是多余的。事实上它确实有些是多余，但在有些情况下，由于缺少检查器或输入约束太强，一种方法可能会错过一个漏洞（例如如果它不在中断或调试命令的背景下进行验证）。还有一种方法s是即使适当的检查器和输入生成器已经到位，也可能无法击中一个漏洞。对于仿真来说，这可能是由于缺乏测试的缘故。

瞄准隐藏案例！

形式验证可以发现大多数类型的漏洞，前提是正确的断言已经到位，输入约束不是太强，并且使用适当的技术来处理状态爆炸（例如抽象）。此外形式化验证在寻找隐藏案例方面也很出色，因为与仿真不同，它将隐藏案例与基本案例同等看待。由于精确时序条件而出现的错误l漏洞，用形式化验证通常比用仿真y验证更容易发现。

仿真验证和形式验证的好与坏？

形式验证在提供 "错误的故障 "时，会受到不良形象的影响。这是因为它在 "无限减 "的基础上工作。事实上，在默认情况下它将达到无限状态。有些状态是不现实的，会通过添加"（减）"的约束条件而被抛弃。如果这些约束不够严格，漏洞出现。如果它们的限制性太强，就会隐藏漏洞。但有一些方法可以确保不会出现这种情况。

另一方面，模拟是在 "零加 "的基础上工作的。除了测试平台允许的行为，没有（"零"）行为会发生（"加"）。仿真也会出现 "错误的失败"（如果测试平台允许错误的输入序列）。隐藏bug的问题也出现在仿真中，而且更加重要。如果测试平台不允许特定的有效输入序列，那么一个漏洞可能会被忽略。

应用于Codasip RISC-V内核的形式验证

在嵌入式内核上使用形式验证技术已被证明是成功和有效的。

编辑：黄飞