基于VC Formal，在RISC-V内核上，验证一波！

Rikki Lu

Sep 05, 2023 / 1 min read

Table of Contents

快速错误检测（QED）
形式化方法与QED相结合的实例分享

验证过程中，如只考虑基本的ISA以及潜在的自定义扩展，该如何为RISC-V内核建立通用的设置，又该如何定义相关的SVA断言？这些SVA断言仅涉及流水线的开始和结束，而不包括内部细节或全流程的所有时钟周期。如果目标是检测单指令错误和多指令错误。单指令错误的发现相对容易，而多指令错误更难识别，因为会遇到CPU停顿事件，这些事件可以避免发生寄存器读写冲突。

单指令错误（例如ADD指令是否真的执行了加法功能）与上下文无关，因此可以通过在其它空流水线中运行该指令来进行检查。但多指令错误却与上下文存在相关性。该如何对所有合法的上下文进行验证？首先需要对QED有一些了解。

快速错误检测（QED）

快速错误检测（QED）最早是为了硅后验证而发明的一种方法。在QED方法中，在机器代码基础上，通过一组并行的寄存器/memory位置定期重复读写指令。然后，比较原始值和复制值；如果二者不同就表示存在错误。这类方法正逐渐运用到前端验证，究其原因，是为了定期比较并行实现一致性，在被一些更具功能意义的断言标记之前，就早早捕捉到根本原因错误。这种方法并不局限于形式化验证，在动态验证中也很有用。

最近的一次网络研讨会重点介绍了形式化方法与快速错误检测（QED）的搭配使用。它赋予了开发者更多处理问题的思路。SyoSil的验证工程师Frederik Möllerström Lauridsen分享了他将这种方法用于新思科技VC Formal，从而对RISC-V内核进行验证的做法。

形式化方法与QED相结合的实例分享

为了使用QED方法，需要参考设计和被测设计（DUT）。这里的参考设计指的是单指令流水线测试，例如通过其它空流水线推送ADD指令。与此同时，DUT将推送相同的指令。但如何将上下文定义为任意选择的前后指令呢？为此，Frederick用到了QED的另一个版本，称为C-S2QED。

无需过多深入技术细节，S2表示“符号状态”，它允许任意指令通过流水线，只要进入流水线的第一条指令与进入参考流水线的指令相同即可。其中“符号”部分是关键。没有必要定义其它指令的推送过程，只要是合法的指令就行。由于使用的是形式化方法，因此验证过程中要考虑到所有可能性。Frederick用到的另一个巧思是首先证明所有指令可在一定的最大周期数内通过流水线，从而为有界证明提供了限制条件。

使用QED方法并利用形式化方法对参考设计和DUT进行比较，证明了流水线实现结果中不存在多指令错误，否则VC Formal会提供反例。Frederick表示，他们还没有将这种方法用到任何标准的RISC-V ISA扩展（M、A、F等）中。但事实上，开发者也可以使用VC Formal DPV来处理M扩展及其它扩展。