形式验证简介

形式验证是一种自动检查方法，可以捕捉许多常见的设计错误，并可以发现设计中的歧义。

形式验证是使用数学技术验证设计正确性的过程。形式验证工具使用各种算法来验证设计并且不执行任何时序检查。这些工具不需要激励或测试台，因此，形式验证在 IC 设计周期的早期执行——即，只要 RTL 代码可用。越早发现错误，就越容易修复。

在英特尔处理器中发现著名的奔腾漏洞后，形式验证开始流行，导致召回有故障的处理器，英特尔不得不承担近 5 亿美元的损失。通过正式验证，可以避免各种其他事件，例如 Ariane 5 爆炸和巴拿马癌症研究所的辐射过度暴露。

硬件系统的许多应用都很关键，其中任何故障都可能导致高额的财务或物理损失。本文讨论形式验证及其各种化身。

目的

形式验证技术跟踪标准验证技术未检测到的错误。此外，对于可以使用标准技术检测到的错误，形式验证通常以明显更快的速度识别它们。在通过仿真和仿真对设计进行功能验证之前，先进行形式验证。

形式验证的一些优点如下：

在设计周期早期检测错误

耗时少

可靠的

快点

详尽无遗

形式验证技术

模型检查

模型检查，也称为属性检查，是一种基于状态的形式验证方法。

以下步骤解释了模型检查的过程：

对系统建模以获得模型 M。系统被建模为一组状态，其中包含一组状态之间的转换，这些转换描述了系统如何响应内部或外部刺激从一个状态移动到另一个状态。

使用属性规范语言(例如 PSL 或 SVA)创建要验证的属性，以得出公式 ɸ。属性是对设计行为的描述。

运行模型检查器以找出模型 M 是否满足公式 ɸ。

如果模型不满足该性质，则生成反例。反例是违反属性的刺激，通常显示为可在仿真中使用的波形。

用仿真中的系统模型运行反例，找出错误的位置。

优缺点

一旦系统模型和属性规范被提供给模型检查器，验证过程是全自动的。但是，就模型检查器要处理的状态数量而言，系统应该很小。

定理证明

定理证明是使用数学推理验证实现的系统是否满足设计要求(或规范)的过程。它是一种基于证明的形式验证方法。

以下步骤解释了定理证明的过程：

将系统建模为形式数学逻辑中的一组数学定义。

从数学定义中推导出系统的属性。

使用定理证明器来验证系统是否符合规范。有各种可用的定理证明器按其基础逻辑分类。定理证明者也可以称为证明助手。

优点和缺点

定理证明的最大优点是它可以处理非常复杂的系统。但是，定理证明不是全自动的，需要人工干预才能完成证明，这需要时间和专业知识。此外，在证明失败的情况下，不会生成反例，这使得定位错误变得困难。

等价检查

等价检查是验证两个设计在功能上是否相同的过程。两种类型的等价检查技术如下：

逻辑等效检查(LEC)：也称为组合等效检查，逻辑等效检查是验证两个设计在寄存器之间具有相同组合逻辑的过程。两个比较的设计也应该具有相同数量的寄存器。该技术用于验证不同抽象级别的两个设计在功能上是否相同;例如，门级网表在功能上与布局网表相同。

顺序等价检查 (SEC)：顺序等价检查是验证两个设计在功能上相同以及在提供相同输入时提供相同输出的过程。SEC 比较了两种设计的时序逻辑，这两种设计可能具有不同的实现方式。这是一个复杂的过程，因此非常受限于设计的大小。

有时，IC 的设计会在最后一刻进行修改，以包含一些功能、时序、电源或其他修复，或者包含一些额外的逻辑，例如扫描逻辑、电源控制电路等。此类更改需要验证。标准验证程序会耗费大量时间，因此会增加上市时间。顺序等效检查将修改后的设计与黄金设计进行比较，并验证它们在功能上是否相同。

总结

形式验证是一种自动检查方法，可以发现许多常见的设计错误，并可以发现设计中的歧义。这是一种详尽的方法，涵盖所有输入场景并检测极端情况错误。

这种形式的验证节省了设计人员的时间和精力，因为甚至在开发测试环境之前就发现了潜在的错误。它可用于设计的高级、RTL 或 GLS 表示。市场上有各种各样复杂的形式化工具，其中许多提供了一种按钮方式来查找设计中的错误。

审核编辑：汤梓红