RISC-V处理器验证：瑞士奶酪模型验证应用

1引言

电子行业对处理性能的要求不断提高，无论是对移动电话等消费设备、智能卡等安全设备，还是汽车等安全关键系统。几十年来，半导体的缩放使新一代系统级芯片（SoCs）能够利用更为密集的通用处理器，直至登纳德缩放定律（Dennard Scaling）结束前，提高处理器速度。 

而今，除了少数应用外，最先进的处理节点对所有应用而言都太过昂贵。在大多数情况下，架构创新是提供更高性能的唯一途径。对于计算要求较高的应用而言，理想情况下，处理器架构应与计算工作负载相匹配。

在SoC上实现的特殊计算单元或加速器可分为两大类。一类是通过向现有处理器内核的流水线上添加附加指令来实现的。在有一组明确定义的算法需要处理，并且对通用处理器提供的广泛服务的需求有限时，此类加速器运行良好。

另一类是处理器模块或协处理器，通过寄存器或内存映射接口与主机通用处理器通信，并对内存有自己的访问权限。

一段时间以来，专用指令集处理器（ASIPs）已经为专门的应用开发。这需要具备足够专业知识的多学科团队来开发指令集、微架构和软件工具链。而很少有公司兼具开发专用指令集处理器的全部技能，所以开发此类处理器的公司相对较少。

随着RISC-V处理器的出现，游戏规则发生了变化，开发专用处理器的门槛大幅降低。现在，设计专用计算单元变得更容易，同时也需要更多的工程师参与进来。虽然RISC-V给处理器设计者带来了好处，但对验证者而言它却提供不了帮助。验证并发现RISC-V处理器上的诸多漏洞几乎等同于使用另一个指令集架构（ISA）来验证处理器。事实上，随着RISC-V推出的新规范和执行逻辑，工程师可能会在无意中创建难以检测的规范和被测器件（DUT）漏洞。随着更多的社区参与开发或修改RISC-V处理器，人们需要对如何有效地验证处理器有更多的认识。

然而，处理器验证从来都不是小事，而是需要结合多种验证技术的优势。这篇技术白皮书讲述了如何通过利用起源于航空电子学界的被称为“瑞士奶酪模型”的多层方法，来有效地验证RISC-V处理器。

2作为架构推动者的RISC-V！

直至最近，SoC设计者仍可以选择使用专有的指令集架构授权一个现成的处理器，或是创建一个专用指令集处理器。大多数公司都缺乏创建专用指令集处理器的资源和技能，因此他们通常别无选择，只能使用现成的处理器。因此，在某些领域，如微控制器，由于基于相同的处理器IP内核，竞争产品之间的差异有限。

专用指令集处理器也有一些明显的缺点。首先，有一个问题是，设计的所有方面，包括指令集，都需要从头开始开发。其次，专用处理器将缺乏软件生态系统。

RISC-V促使生态系统变革，它具有开放、模块化、可定制的优点，并且它的标准仅涵盖指令集架构。这种开放性意味着设计师团队不局限于单一供应商，整个软件生态系统都可以使用该标准。这使得RISC-V生态系统得以迅速发展。

模块化意味着人们可以根据需求选择自己想要的标准扩展，使处理器能够根据应用调整不同的配置。通过创建自定义指令来优化目标工作负载的执行，可以实现更细粒度的调优。这种将RISC-V指令集架构与预期应用相匹配的自由提供了极大的创新机遇。

由于RISC-V开放标准只涵盖了指令集架构，因此对使用它的微架构没有任何限制。因此，在执行单元、流水线长度、缓存等方面可能存在差异。

在许多情况下，最快速开发专用RISC-V处理器的方法是从一个相当接近于满足需求的现有处理器设计开始，然后进行定制设计，例如，创建自定义扩展。 

一种可能是从开源RTL实现开始，然而，修改RTL，更新指令集模拟器（ISS）和软件工具链都依靠手动操作，这也就意味着需要更多的劳动力，且更容易出错。

Codasip使用 CodAL架构描述语言开发其处理器。通过高水平的描述这一设计并使用Codasip Studio设计自动化，可以自动生成RTL、软件工具链和验证环境。授权Codasip的 RISC-V 处理器的CodAL架构来源是定制化的有效起点（图1）。

图1: 可以定制RISC-V处理器的CodAL描述，以满足应用的需求

但是，通过定制现有处理器，需要进行额外的验证，因为定制的处理器与原始处理器不同。尽管预先验证的现有处理器是一个非常好的起点，但在验证中切忌自满。

3处理器和软件复杂性

许多SoC工程师都熟悉RTL模块的验证。他们熟悉使用约束随机验证或形式化验证等技术来运行个人识别码的程序块。

那么，处理器验证也是同样的挑战吗？执行软件将处理器与硬连接逻辑区分开来。软件变体意味着许多不同的指令排列组合将被应用于处理器。它们必须被准确地执行。

软件的复杂性也差别很大。例如，一些处理器深深嵌入芯片中，这意味着芯片的用户无法更改处理器上运行的软件。在其他情况下，SoC中的嵌入式处理器可以由终端用户进行编程。在第一种情况下，处理器需要与来自SoC开发商提供的少量软件一起工作，而第二种情况则必须与来自第三方开发商提供的多种软件以及多个实时操作系统（RTOS）一起可靠地工作。

在高端应用方面，处理器必须能够运行富操作系统，诸如Linux或安卓。此外，大量的应用将在处理器上运行，特别是在安卓系统中，谷歌应用商店有数以百万计的不同应用。

与硬连接逻辑的另一个区别是，处理器的执行可以被外部异步事件中断。处理器必须在许多指令和外部事件的排列组合下正确运行。 

此外，处理器故障的后果千差万别。如果消费类无线芯片的设计错误导致一些数据包的丢失，那么通信协议可能会妥善地纠正该问题。但是，如果处理器的设计错误导致安全元件受到破坏，那就可能导致密码或金额被盗。如果是嵌入汽车或医疗系统的处理器，那么设计错误可能会导致人员伤亡。

简而言之，与大多数硬连接逻辑块相比，处理器有巨大的状态空间来进行验证。验证是处理器设计周期中最重要的组成部分。

4处理器漏洞

处理器漏洞——特别是那些导致产品召回的漏洞——有时会出现在公众的意识中。早在1994年，英特尔就因为FDIV浮点运算缺陷而召回了奔腾处理器。2017年，一些与安全缺陷相关的漏洞，如“熔断”和“幽灵”，影响了大量使用推测执行机制的处理器设计。

大多数处理器漏洞从未受到公众关注，而大多数处理器用户会惊讶地发现，设计一个典型的中端处理器需要在RTL代码中修复1000个漏洞。使用诸如无序执行之类的高级特性，漏洞的数量可能会更多。虽然这个数字听起来很庞大，但重要的是要记住，漏洞在复杂性上有很大的差异。

4.1漏洞分类法

正如生物学家将动物和植物分为类和种一样，将漏洞分门别类（四类）也很有用。

4.1.1简单漏洞

漏洞源于人为错误，其中一些很容易被设计师和验证工程师发现。举一个典型的例子，在编译阶段就能发现的语法错误，比如缺少一个分号。

为了避免这类错误，设计团队必须仔细阅读规范，并在开发过程中关注规范的任何更改。另一方面，验证团队需要进行全面检查规范的测试。

另一个例子是规范的一部分没有实现。如果为规范的这一部分编写了特定的测试，那么任何像样的测试平台都应该能够找到它。

当使用获得商业许可的现成处理器时，设计者假设RTL与指令集架构完美匹配。对于RISC-V，情况也是如此，因为指令集架构是模块化的，支持自定义指令。

如果设计了一种新的RISC-V处理器，那么就有开源的指令集模拟器（ISSs）可用，如Spike。如果使用了RISC-V指令集架构的合理标准配置，如RV32IMC，那么指令集模拟器可以作为确保RTL符合指令集架构的标准参考。然而，在添加自定义指令时，情况会变得更为复杂。

如上所述，如果一个定制的处理器或/加速器是通过修改现有的RISC-V RTL实现的，那么同时更新指令集模拟器和RTL就有可能导致错误。

因为Codasip Studio根据其高级描述生成RTL，并且该合成引擎已经在许多项目中测试，因此生成的RTL不太可能包含由低级编码错误导致的漏洞。

通过使用通用验证方法学（UVM）对指令集模拟器的标准参考进行验证，可以检查修改后的设计RTL是否符合扩展的RISC-V指令集架构（图2）。不仅是应用软件，随机生成的汇编程序也可以用来刺激UVM环境。而由于处理器的状态空间很大，执行大量的排列和指令组合是很重要的。

图2：检查合成的RTL与标准IA参考的一致性是处理器验证中的一个关键检查

同样需要多加注意的是，覆盖率报告不会发现RTL中未实现的特性。

然而，以规范为参考的代码审查肯定有助于发现规范中未实现的部分。

综上所述，应通过运行一个检测来测试处理器特性，从而发现简单漏洞。任何不良行为都是系统性的，而非一个计时条件。

4.1.2边角案例漏洞

如上所述，用相当简单的测试用例就可以检测到很容易发现的漏洞。即使简单的同步测试用例在随机延迟的情况下执行，它们也可能通过测试，而错失真正的漏洞。

边角案例漏洞的查找则更复杂，需要一个强大的测试平台。发现这样的漏洞通常意味着异步事件。例如，执行一个中断指令，且该指令恰好在另外两个特定计时的指令之间到达。处理器内部还存在其他事件，比如数据结构中的先入先出队列（FIFO）异常，就可能会对处理器的另一个程序块施加压力。为了找到这样的漏洞，有必要使用一个测试平台，在指令、参数和延迟上做文章，以便实现所有可能的指令和事件的交错。一个优秀的检验员应该能发现偏离预期的情况。

其他类型的边角案例包括功能错误，如数学上溢/下溢或对异常地址的内存访问。对推测性执行的验证尤其具有挑战性。

同样，代码覆盖率的价值也是有限的。这是因为一个漏洞的条件是几个已经单独涵盖的事件的组合。条件或分支覆盖可能会有所帮助，但很难分析。 

4.1.3隐藏漏洞

一些漏洞无法通过所使用的初始处理器验证方法检测出来。在糟糕的情况下，它们会被客户当场发现，而在最坏的情况下，需要召回芯片。应用额外的验证层可以降低这些漏洞逃过检测的概率。

通过使用多个测试平台或验证环境，可以发现更多的漏洞，因为刺激不同。然而，使用随机测试平台方法所能达到的效果是有限的。

在随机刺激下，测试平台倾向于生成类似的东西。

这就好比掷骰子，连续10次掷出6的概率非常低——精确到6000万分之一的概率。如果一个RISC-V处理器支持100条不同的指令，并且有10级流水线，那么在所有流水线都出现相同指令的情况下对其进行测试也不是没有道理的。那么，对于一个等概率随机指令生成器来说，这种可能性有多大？产生这个序列的概率只有1020分之一！

必须调整随机约束，以覆盖所有更深层次的情况为目标。

4.1.4发现越来越多的漏洞

总而言之，寻找漏洞通常是一个渐进的过程，来处理愈发难以找到的漏洞（图3）。在设计过程中，验证方法的复杂性通常会增加。较简单的方法会成功地发现简单漏洞，而更强大的测试平台则需要找到边角案例。正如第5节中所述，需要结合多种方法来找到最困难的隐藏漏洞。

图3：越来越先进的验证方法发现了越来越多的漏洞

及时发现漏洞，尤其是隐藏漏洞，对于一个成功的处理器开发项目至关重要。如果太晚发现项目中的漏洞，那么上市时间将受到不利影响。

4.2评估漏洞复杂性

在设计或定制处理器时，一个显而易见的问题是询问处理器的验证何时完成。换句话说，如何衡量测试平台的效率？验证结果的可信度如何？业界通常使用的指标包括覆盖率和漏洞曲线。虽然这些措施是必要的，但它们不足以达到尽可能高的处理器品质。它们未能揭示验证方法找到最后一个漏洞的能力。

4.2.1定义漏洞复杂性

漏洞复杂性已被证明是整个处理器开发周期中验证有效性的一个较好指标。

我们所说的漏洞复杂性是指击中漏洞所需的独立事件或条件的数量。

举一个简单的例子。当数据依赖关系在设计中没有正确实现时，在缓存中会发现一个典型的漏洞。此时数据损坏可能发生在以下情况：

1.地址@A中的高速缓存行在高速缓存中状态为“valid”及“dirty”。

2.地址@B的加载会导致A行的驱逐。

3.在地址@A开始进行另一个加载。

4.外部写总线比读总线的速度慢，因此@A的加载在驱逐结束前完成。

外部存储器返回以前的数据，因为来自驱逐的最新数据丢失了，导致数据损坏。通常，设计应检测到这种情况，并确保正确的数据处理。

在这个例子中，需要四个事件或条件来击中该漏洞。这四个事件给漏洞打了4分，或者换句话说，漏洞的复杂性为4。

4.2.2漏洞的分类和复杂性

在第4.1节，我们考虑了如何根据漏洞的特征对它们进行分类。

一个简单漏洞需要通过一个简单的测试来触发一到三个事件。然而，一个边角案例将需要触发四个或更多的事件。参考第4.2.1节中的例子，如果这四个条件中的任何一个不存在，就不会检测到该漏洞。要使用一个约束随机测试平台来检测漏洞，则该平台需要具备以下特性：

a)地址序列必须足够智能，可以重新使用之前请求的地址，

b)外部总线上的延迟应包含足够快速的读写，

c)外部总线上的延迟应包含足够慢的读写。

隐藏案例则需要更多事件来触发。例如，我们借用第4.2.1节中的例子，再额外增加了复杂性，即它只发生在缓存中发现错误检查和纠正（ECC）错误（5），与中断恰好同时发生（6），并且只有当处理器完成浮点处理单元（FPU）操作导致除零错误（7）的时候。在典型的随机测试平台中，所有七种条件同时出现的概率非常低，这使得它成为一个“隐藏的”漏洞。

这种漏洞的分类和复杂性没有任何限制。经验表明，一个能够找到8分或9分漏洞的测试平台确实是一个非常强大的测试平台，并且是提供高质量RTL的关键。最先进的模拟测试平台能够找到复杂性级别高达10的漏洞。好消息是，形式化验证使找到复杂性更高的漏洞变得更容易，这为更好的设计质量铺平了道路，并为如何改进验证提供了线索。

5用于处理器验证的瑞士奶酪模型

处理器都有高品质的要求，其品质是处理器验证团队主要关注点。在优化资源使用的同时，验证需要有一个足够全面的范围。在进入大规模生产之前，找到关键的处理器漏洞是至关重要的，因此验证必须足够彻底。另一方面，这个过程必须是高效的，以满足上市时间的要求。

5.1用于验证的思维模式

开发高质量处理器IP的出发点是拥有正确的验证思维模式。为了达到一流的品质，验证团队的思维模式可以在一个强大的验证计划和一组测试之间产生差异，这将捕捉到漏洞，并生成一份漂亮的覆盖率报告，但却无法发现更深层次的边角案例漏洞。为了达到较高的RISC-V设计质量，有必要采取这样的思维模式，即任何一种验证方法本身都不足以支撑整个验证。与之相反，必须应用不同的验证方法来不断改进漏洞检测，包括代码审查、智能随机验证、操作系统（OS）引导等。

5.2起源于航空领域的瑞士奶酪模型

Codasip认为，为了实现这些目标，有必要结合所有行业标准的验证技术——并通过瑞士奶酪模型联系起来。瑞士奶酪模型出现在有严格安全要求的航空领域。这一模型是基于与埃曼塔奶酪切片的类比。众所周知，埃曼塔奶酪以具有大小孔的组合而闻名（图4）。假设有一组可能导致飞机事故的危险，而每一片奶酪代表一种危险检测方法。 

图4：在瑞士奶酪模型方法学中，较小的孔代表良好的检测方法。较大的孔洞代表一种相对不很严谨的方法。

为了避免飞机坠毁的风险，航空业对程序、飞行检查单和冗余系统要求非常严格。如果有一条直接穿过所有切片的路径，飞机就有坠毁的风险。用任何一种方法都会有一些危险未被发现，但如果有足够大的奶酪切片组合，那么所有重要的危险都可以被发现。

5.3应用于处理器验证的瑞士奶酪模型原理

同样的分层方法也适用于处理器验证，其起点是将用于综合设计的RTL代码。可以应用多个验证层，以确保在发布处理器IP之前检测到漏洞（图5）。如果改进一个给定的验证方法，那么“孔”的大小就会减小。切片的不同部分可以视为设计的不同部分。

图5：瑞士奶酪验证方法在设计周期中结合了多种验证方法

结合多种验证技术涉及一些冗余，但通过使用互补的方法，可以最大限度地减少漏洞逃脱的风险。 

通过使用不同的奶酪切片或验证方法，我们有以下好处：

1.冗余确保了在某一层失败时的连续性。

2.当在开发过程中发现漏洞时，就表明漏洞出现在了其中几片奶酪上。改进验证方法可以减少每片奶酪上的漏洞大小。我们提高了检测漏洞的几率，无论是简单的漏洞，还是复杂的边角案例漏洞。

3.最大限度发挥每种验证技术的潜力。

奶酪片上的一个孔洞就类似于验证方法中的一个洞。洞的数量越多，体积越大，则逃脱检测的漏洞就越多。如果设计的相同区域（奶酪片）没有被任何验证技术所覆盖（切片之间的重叠孔），那么这个漏洞就会通过验证，并可能在最终出现在交付产品中。一种好的验证方法应呈现尽可能少且小的孔。坚实的战略、丰富的经验和高效的团队沟通是交付高质量产品的重要因素。

瑞士奶酪模型在受到持续改进时最为有效。当发现漏洞时，我们可以从用于查找漏洞的场景和检查中吸取经验教训。虽然改进用于查找漏洞的那一层上的场景和检查程序很重要，但同样重要的是看看是否可以将经验教训应用于其他验证层。这就类似于减少多个奶酪片上的孔的大小。

图6：瑞士奶酪模型的迭代改进可提高验证质量。这是一个良性循环。

5.4准备开始

验证的一个良好起点是对被测器件RTL和初始测试平台进行代码审查。代码审查可以很容易地发现一些简单漏洞，例如规范中错误实现的部分。由于规范在设计周期中可能会发生变化，因此务必确保任何更改都已反映在代码中。

另一个早期的检查是验证处理器内核是否符合所需的指令集。完整性检查是实现这一目标的有效方法，例如，通过将设计与行业标准模型进行比较；Codasip使用的切片之一。与此类模型相比，作为标准参考，提高了Codasip RISC-V处理器的质量，并且这些模型中的漏洞已经被报告，以提高RISC-V的整体质量。如果通过添加自定义指令修改了处理器，则标准参考必须包含这些额外的指令。

处理器的RTL是分层的，因此除了在顶层运行定向测试之外，在设计层次中的较低层次创建块级测试平台以检查正确的操作是有意义的。

5.5改进瑞士奶酪模型

虽然瑞士奶酪模型——由于是多层次的——本身就能很好地发现处理器漏洞，但在项目过程中改进这些层是很重要的。当发现一个错误——在切片验证中的一个孔时——应该修复它，并检查其他切片是否有类似的孔。给定切片发现的漏洞也应帮助在其他验证切片中找到漏洞，这些漏洞应该在进一步进展之前得到解决。 

单一的验证技术不能依靠其本身找到每个漏洞，而是所有验证技术的综合提高了验证的整体质量，从而提高了整体处理器的质量。

同样重要的是要记住，设计不是静态的（除了漏洞修复之外），在产品的开发过程中可能会有意外的变化或外部因素影响验证。例如，设计团队没有向验证团队传达设计变更。同样地，一个沉闷的周五下午的工作也可能会导致人为错误，从而降低验证质量。

这样的人为错误会增加切片上的孔的大小，并降低验证的有效性。

重要的是不要仅仅依赖一个验证层，而要保持工程规范的更新，让设计和验证团队良好沟通。 

只有将应用漏洞复杂性和以下改进方法贯穿项目开端和整个设计开发过程中才有用。这有两个原因：

1.必须在发现漏洞时进行修复。如果2级或3级的漏洞未被修复，就意味着在启动大规模浸泡测试时将会发生很多故障。据统计，来自同一集群的类似漏洞，除非有更多的事件触发，才可能会被注意到。

2.漏洞复杂性被用来改进和衡量测试平台的质量。由于复杂性级别与触发漏洞所需的事件数量相匹配，因此复杂性得分越高，测试平台就越严格。追踪和分析触发漏洞的事件对于了解如何调整随机约束或创建一个新的功能覆盖点非常有用。

5.6使用智能随机测试击中漏洞集群

处理器漏洞的一大特点是，它们很少单独出现。事实上，就像昆虫一样，虫子通常是成群结队的。换句话说，当通过定向测试在设计的给定区域发现一个漏洞时，在设计的同一区域很有可能有更多具有类似条件的漏洞。

如果发现了一个新的处理器漏洞，那么它不应该是验证之旅的结束，而是一个找到更多漏洞的机会。 

这个漏洞应该被用作一根指针，帮助查找同一区域的更多漏洞。它应当是找到整个漏洞集群的提示。

试想一下，一个顶级随机测试在经过数千小时的测试后发现了一个漏洞。这个漏洞很可能是由以前从未遇到过的事件组合发现的。这很可能由外部修改引起，例如，测试中参数的更改、RTL修改或模拟器修改。

通过发现这个罕见的新漏洞，很明显会有一个更严格的测试平台，用来测试一个新的设计领域。

然而，在测试平台被改进之前，这个设计领域并没有被强调。如果我们认识到漏洞成群结队出现，那么这个区域就需要进一步的探索来找到更多的漏洞。

为了击中这些漏洞检查器，我们可以添加断言和测试。来看这个测试，如果这个漏洞通过定向测试再现，那么只有完全相同的漏洞才会被击中。与之相反，在同一区域很可能有其他具有类似条件的漏洞。为了扩大打击漏洞集群中其他漏洞的范围，可以使用智能随机测试。请注意，正常的无目标随机测试在这种情况下无效，因为给定的漏洞集群模式有一个明确的目标。

如果这个漏洞是在一个特定的RISC-V指令上发现的，那么一个合理的问题是，是否可以通过增加该指令的测试概率来改善测试呢？乍一看可能是这样，从统计学角度分析，失败越多，暴露的漏洞也会越多，但大多数漏洞都是通过一系列罕见事件的组合发现的。此类事件的例子包括停滞的流水线、完整的数据结构中的先入先出队列（FIFO），或者其他一些微架构的细节。

标准的测试平台可以通过简单地改变一个测试参数来调整指令的概率。然而，充满FIFO通常是不可能的。当测试平台仅通过改变一个参数来针对性地充满FIFO，以触发其他独立参数（如延迟）的组合时，测试策略可以得到明显改善。

对于一个设计中新发现漏洞的区域，智能随机测试通过将搜索范围扩大到设计的邻近区域，来有效地发现更多的漏洞。它包括通过调整多个参数来调整测试，以激活更多触发漏洞的事件。虽然这看起来很耗时，但这种方法在提高测试质量和处理器的质量方面很有效。

5.7随机测试后检查覆盖率

覆盖率是著名的“覆盖率驱动验证方法”的反馈回路。它在随机刺激的情况下特别有用。由于是随机的，验证工程师只控制应用于被测设备的不同模式的权重。在不同种子的帮助下，随机生成模式将被组合起来，并在模拟过程中被应用到设备上。但是，需要多少不同的种子才能确保处理器的测试呢？测量覆盖率作为一个度量标准，可以让人相信随机生成器已经生成了所有需要的情况。

特别是，它应该对之前进行的随机验证步骤的质量给出反馈，无论是在顶层还是区块级别。

代码覆盖的类型包括：

●语句覆盖

●条件/表达式覆盖

●分支/判定覆盖

●翻转覆盖

●状态机（FSM）覆盖

如果在代码覆盖中发现漏洞，则需要设计进一步的测试来运行代码的这些部分。

功能覆盖是确保模式执行特定功能的另一个重要部分，传统的代码覆盖不一定能测量。它在以下两个领域尤其有效：

-架构覆盖（确保执行了各种类型的指令，并结合各种中断的情况）

-微架构覆盖，以确保对罕见的功能进行深度测试。

5.8使用形式化验证来搜索隐藏漏洞

虽然智能随机测试可以用来扩大被测试的设计区域，但重要的是要明白随机测试并不是彻底的。最新的漏洞可能出现在现有测试平台未覆盖的区域，或者需要通过一个天文数字周期的模拟才能被找到。这种情况类似于在夜晚寻找一个丢失的物品。

图7：传统模拟类似于在一盏路灯下寻找丢失的物品，但形式化验证类似于在有充分照明的街道上寻找。

传统模拟可以类似于在一盏路灯下寻找。然而，大部分的街道空间都处在黑暗之中。智能随机验证可以扩大照明区域，但不能到处搜索。形式化验证可以彻底地搜索，此种形式类似于在有充分照明的街道上进行搜索。

模拟需要投入促进因素的开发。相比之下，形式化验证不需要在促进因素方面下功夫，但需要限定足够的检查。

因此，形式化技术是瑞士奶酪模型中的一个关键部分。通过在覆盖下使用详尽的分析，并以形式化术语反映被测器件的规范，可以发现未预见到的设计路径，这些路径中隐藏着其他验证方法所不能揭示的漏洞。

通过为每个指令使用一组专用的操作断言模板，可以实现高度的自动化。具体来说，这种方法使用了SystemVerilog断言（SVA）的扩展，该断言提供了高层次的、不重叠的断言，以捕获端到端的事务和需求。这种简明、流畅的方法的优势包括：

●能够转化功能要求，以自动检测规范的遗漏和错误，以及验证计划中的漏洞和未经验证的RTL功能。

●以简明流畅的方式捕获整个电路事务，类似于时序图。

●将特定实现的支持验证代码与可重用的规范级代码清晰地分开。

●通过高层次和易于审查的断言，实现100%的功能覆盖。

来看看以下在处理器设计中验证RISC-V FSQRT行为时遇到的真实例子。RISC-V指令集手册中对指令字段的定义如下：

图8：RISC-V FSQRT指令格式

该标准要求源寄存器字段rs1为“0”，以使指令有效（图8）。形式化验证发现了一个反例，在这个反例中，编码为rs1不等于“0”的指令被错误地解码为FSQRT，而不是未定义。

图9：一致性检查发现由硬连接信号引起的死码。

另一个关于自动一致性检查如何识别潜在漏洞的例子如上图所示（图9）。第一个代码片段（左）显示了一个依赖于流水线控制器代码片段（中）中的信号的分支。形式化检查标记了信号s_ex1_clear被绑定为零（右侧片段），这意味着该分支是不可执行的。

5.9通过使用现场可编程逻辑门阵列（FPGA）操作系统启动来给设计施加压力

许多提及的瑞士奶酪方式方法都涉及到RTL的模拟。这很容易设置，但其缺点是相对较慢。这意味着，即使模拟运行数天，完成的处理器时钟周期数也相对较少。RTL模拟器的运行速度范围平均为每秒数百或数千条指令。

处理器设计的FPGA实现将比RTL模拟快得多，尽管比SoC实现慢。对于处理器的设计，使用FPGA可以达到10-50兆赫的速度。为了创建原型，有必要合成处理器子系统，并从FPGA板的内存中运行代码。其周转时间高于RTL模拟。

使用处理器的FPGA实现允许以比模拟多几个数量级的时钟周期来执行设计。这种奶酪层的一个典型应用是启动操作系统，并运行各种压力测试，以便在现实的场景中来运行设计。

6结语

RISC-V作为一个开放的、模块化、可定制的指令集架构，为架构创新提供了新的机会。

然而，只有具备足够的验证策略，这种机会才能通过现代SoC设计所需的质量来实现。随着越来越多的团队参与RISC-V开发，越来越多的工程师需要精通处理器验证方式方法。

Codasip提供了一种涉及多种验证方法的多层方法，以实现优越的处理器质量水平。这种瑞士奶酪模型的方法类似于在航空电子学中为确保高水平的可靠性和飞行安全而采取的做法。该方法在设计周期中迭代的改进验证层，以最大限度地提高漏洞检测的概率。瑞士奶酪验证层的迭代改进是支持提高处理器质量的良性循环。

对于定制的RISC-V处理器，可以采用相同的方法，但要以经过验证的处理器为起点。

审核编辑 ：李倩