关于形式验证的11个误区

形式验证如何在 signoff之前发现bug。

形式化验证在数学上能够详尽地证明一个芯片设计符合一组断言的能力。

形式化技术是当今芯片成功设计、验证和实现的核心。

形式化验证的优点在芯片开发中是众所周知和公认的。但事实并非总是如此；几十年前，形式技术被广泛认为是一种需要“魔法”才能在实际项目中成功使用的外来技术。在这段时间里，许多在signoff前发现的真正可怕的bug的成功故事，帮助提高了人们对形式验证的认识和信心。 用数学方式详尽地证明芯片设计满足一组断言的能力与仿真形成鲜明对比，仿真不能证明没有bug。如果由于合法的设计方案违反了断言而不能实现证明，形式化工具就会把这些作为反例提出来，并提供信息以帮助设计者调试它们。用户提供约束条件，使形式化分析保持在合法范围内，确保反例是在硅片后使用中可能发生的的真实故障场景。 这一切听起来很好，那么为什么不是每个人都在运行形式验证呢？它每天都被数百家芯片和系统公司的数千人成功使用，但一些设计者和验证工程师仍然不情愿。这可能部分是由于一些持续存在的关于形式化技术的误区所致，使它看起来太难或太昂贵。这篇文章研究了这些误解，并解释了为什么它们不应该成为担忧的原因。1. 您需要博士学位才能使用形式验证。对于第一代形式化工具来说，这个误区可以说是正确的，这些工具是为学术目的而设计的。他们需要学习一种晦涩难懂的数学符号来指定断言和约束。这些工具需要大量的手动指导，所以大多数用户实际上是专门研究形式验证技术的教授和博士生。 比如考虑RISC-V弱内存模型的负载值公理。它表示，对于线程i、j和k，如果线程i执行一个STORE操作，接着线程j执行另一个STORE操作，然后线程k执行LOAD操作，那么LOAD从内存中检索的值将是STORE更新的最新值。形式上，数学上精确的符号可以表示这一点，如图1所示。然而，一个普通的设计或验证工程师可能无法理解这些符号，它们对形式方法博士来说是友好的，但对其他人来说则不然。

  1. RISC-V弱内存模型的负载值公理示例。 不过近年来发生了很大变化。断言和约束通常使用 SystemVerilog 断言 （SVA） 指定，SVA 是设计人员和验证工程师已经知道和使用的 SystemVerilog 语言的子集。正式工具变得更加智能和独立，并且更少依赖用户专业知识。现在，许多都为调试反例或帮助实现完整证明提供了可视化和更好的提示。不需要博士学位。 还有一大类形式化应用（App），通常不需要用户编写任何断言。例如，一个时钟域交叉（CDC）工具可以自动确定芯片中出现交叉的位置，以及必须证明哪些断言以保证正确的操作。用户只需要提供一些关于时钟的信息，其中大部分信息在综合和布局工具使用的约束文件中已经存在。2. 形式化验证很难，因为你需要形式化专用的规范。规格说明对于其他形式的验证(如模拟或仿真)是不必要的，这是不正确的SoC 仿真中的固件和驱动程序堆栈已经提供了合适的环境来将激励驱动到芯片中进行测试;检查程序依赖于需求来确定在运行测试时需要发生什么。如果没有规范，验证工程师就不能为模拟、通用验证方法(UVM)或功能覆盖编写定向测试。 形式化方法对规范明显更敏感，因为定义不明确的需求的影响更加严重。形式化测试（指定为断言、约束和覆盖）会产生意想不到的结果，因为形式化工具驱动激励模式的所有可能组合。如果从需求中捕获的约束不准确，这可能会导致驱动虚假激励。 在许多情况下，从规范派生形式验证需求的行为可能会暴露bug。事实上，一个好的规范是成功的形式化验证的一个隐藏的条件（图2）。

2.  Better specifications are a hidden bargain for formal verification3. 您无法将形式化技术扩展到大型设计。这是前几代形式技术的另一个误区;用户仅限于分析小型设计块。今天的形式验证工具具有更大的容量，并且许多工具能够在服务器或云上以分布式模式运行。形式验证的技术和方法也得到了扩展。 设计人员和验证工程师通常会将形式验证应用于大型复杂子系统，包括端到端地验证整个多线程 64 位处理器。图 3 显示了基于 Axiomise 抽象的解决方案在具有超过 10 亿个门（3.38 亿触发器）的高度参数化片上网络 （NoC） 中捕获的bug示例。

  3. 这个功能漏洞，在一个有超过 10亿个门的设计中，是 Axiomise 使用 CadenceJasperGold 发现的。 形式化应用程序可能具有更大的容量，因为它们专注于单个任务。例如，CDC分析始终在全芯片上运行，以检查整个时钟网络。4. 形式验证需要很长时间才能收敛。在某些情况下可能会发生这种情况，尤其是当形式测试testbench没有自然设计为最佳性能时。但是，在大多数情况下，形式属性收敛得非常快。 当然，形式验证工具的运行时间取决于设计大小、设计复杂性以及断言和约束的数量。有多种方法可以管理形式验证流程以保持运行时合理。随着设计的增长以增量方式运行和在分布式模式下运行都有帮助。5. 形式化技术只对构建证明有用。这个误区也源于学术形式工具，其中的重点完全是实现完整的证明。虽然完整的证明为设计正确性提供了最大的信心，但形式验证通过发现棘手的极端情况bug（如图 4 中的示例）来增加价值。

  4. 端到端RISC-V形式验证：使用Axiomise formalISA，在本例中，使用西门子的QuestaPropCheck，在30分钟内完成50%。 图 5 所示的波形显示了使用 Axiomise 形式验证解决方案在 ibex RISC-V 内核中捕获的bug。仅当调试请求在控制器 FSM 处于解码状态时以相同的时钟周期到达时，此Bug才会出现在设计中。该Bug不会以任何其他状态显示。调试到来的精确时间将使这种bug很难通过动态仿真来捕获，其中激励的可控性和详尽的覆盖范围将是一个重大挑战。

  5. 由于 ibex RISC-V 内核中的bug而导致 BEQ 指令失败，仅当FSM 控制器处于解码状态时，才会由传入的调试请求触发。6. 如果您以 100% 的覆盖率运行了模拟仿真，则不需要正式的技术。如前所述，形式验证非常适合查找模拟或仿真遗漏的极端情况bug。此外，这个误区夸大了覆盖指标的价值。它们在识别尚未执行的设计部分方面非常有价值，在这种情况下，不可能找到所有bug。 但是，如前所述，仿真无法建立详尽的数学证明。即使是 100% 的功能覆盖率也不能保证没有bug逃逸——它只是确认了所选指标所涵盖的设计部分的实践。正式分析将考虑所有可能的行为，并且很可能会发现其他bug。7. 形式化技术只对查找极端情况的bug有用。许多形式化的用户对形式化的bug搜索深信不疑，有时甚至使他们的管理层认为形式化只适合于bug搜索。形式化最大的好处之一是确定在设计中不存在与形式化证明的需求有关的bug。 例如，考虑一下RISC-V。许多以前通过仿真验证的处理器最终都有bug逃逸，然后被形式化抓住。形式化可以毫无疑问地证明，一旦bug被修复，就不存在bug了，因为形式化的属性证明了设计的所有可达到的状态（图6）。

  6. 这种情况下与JasperGold 一起使用的 Axiomise formISA 应用程序如何用于查找bug并构建架构正确性证明，以便对 64 位 RISC-V 处理器进行端到端验证。 当然，没有什么比发现一个深层的、可怕的、需要翻转芯片的bug更能证明形式化的力量了。一个验证工程师说 "我们在模拟仿真中永远不会发现这个问题"，很快就会让人相信形式化。 但是形式验证可以更快地发现各种bug，包括通常在仿真中发现的bug。出于这个原因，今天的芯片项目通常包含多个区块，其中一些区块相当大，无需任何区块级仿真即可正式验证。8. 一旦你应用了形式化技术，你就不需要模拟及仿真了。通常，每个形式验证环境都使用约束来描述接口。这些约束需要在仿真中验证，以检查它们是否被正确建模和解释以进行形式验证。 此外，形式通常在流程的早期应用，以获得验证shift-left的最大值。当设计成熟并编码更多模块时，某些接口约束可能不再有效，因此必须在仿真中重新验证它们。 此外，仿真和形式化对于查找与硬件-软件交互相关的bug很有价值，这些bug仅在软件在嵌入式或主机处理器上运行时在模拟或仿真中发生。同样，模拟-数字接口上的bug可能仅在运行混合信号仿真时发现。9. 形式化技术不提供任何覆盖指标，因此很难知道您是否做得足够多。这显然是不正确的，因为证明提供了一种形式的覆盖指标。知道设计中100%的断言永远不会被违反，这显然是一个强有力的声明。 但是，所有现代工具现在都会生成与形式展示中经过验证的断言相关的代码覆盖率视图（图 7）。它显示了在形式证明期间激活并运行了哪些设计代码行。

  7. JasperGold 覆盖 32 位 cv32e40p 处理器的检查器覆盖率应用程序显示，已通过 RISC-V 的 Axiomise 正式ISA 应用程序验证。 以前使用形式工具在没有任何形式检查器的情况下评估代码覆盖率。他们仍然可以提供对无法访问和死代码的见解，这可能是由于设计代码或配置冲突的结果。正式工具还广泛用于证明UVM环境中无法访问的代码覆盖漏洞可能始终无法访问，或者可能会在UVM中发现覆盖差距。 Axiomise 开发的六维覆盖流程描述了如何从定性和定量上计算形式覆盖率（图 8）。

8. 正规覆盖的六个维度。10. 模拟仿真和形式验证不能合并使用。如前所述，这两种核查办法是相辅相成的。每个人都可以找到对方可能不会找到的某些类型的bug。没有一个芯片项目运行一个而没有另一个。可以将其视为假设接口假设以保证形式验证中块不存在bug，然后在仿真中验证假设以关闭完整的循环。 此外，在仿真中使用形式化来建立覆盖差距是结合这两种技术的一个很好的例子。许多跟踪覆盖率结果的项目管理工具从模拟和形式验证中收集指标，以提供验证进度的统一视图。这有助于让老板相信团队正在满足指标驱动验证的要求。11. 形式化技术仅对功能验证有用。断言、约束、详尽的数学分析、证明和反例的一般概念出现在芯片开发领域，而不仅仅是检查功能正确性。 如今，形式验证工具被广泛部署用于验证架构需求、CDC、连接、电源、死锁、微架构功能需求、安全性、安保和 X 传播（图 9）。

  9. 形式验证的普遍使用。 在DAC 2021上展示的最新示例显示了如何使用形式验证来查找RISC-V内核中的安全漏洞（机密性，完整性和可用性），并根据漏洞评分对其进行排名。安全性的最大挑战是处理未知的攻击场景。这就是形式真正闪耀的地方，因为它引入了各种输入激励，试图做到详尽无遗，找到设计师通常永远不会考虑的场景。 部署正式的行为迫使设计师和架构师考虑在架构开发的早期阶段利用漏洞，避免下游出现任何的意外。 形式化技术是当今芯片成功设计、验证和实现的核心。随着11个误区的消除，相信您将会毫不犹豫的接受形式验证技术。    

审核编辑 ：李倩