用数学办法详尽地证明芯片设计知足一组断言的能力与仿真形成光鲜比拟，仿真不能证明没有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 verification
3. 您无法将形式化技能扩展到大型设计。
这是前几代形式技能的另一个误区;用户仅限于剖析小型设计块。本日的形式验证工具具有更大的容量，并且许多工具能够在做事器或云上以分布式模式运行。形式验证的技能和方法也得到了扩展。设计职员和验证工程师常日会将形式验证运用于大型繁芜子系统，包括端到端地验证全体多线程 64 位处理器。图 3 显示了基于 Axiomise 抽象的办理方案在具有超过 10 亿个门（3.38 亿触发器）的高度参数化片上网络 （NoC） 中捕获的bug示例。3. 这个功能漏洞，在一个有超过 10亿个门的设计中，是 Axiomise 利用 Cadence JasperGold 创造的。形式化运用程序可能具有更大的容量，由于它们专注于单个任务。例如，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个误区的肃清，相信您将会绝不犹豫的接管形式验证技能。
