形式验证简介及其三种技术形式

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

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

形式验证的普及得益于英特尔处理器中发现的著名的奔腾漏洞，那次事件导致故障处理器被召回，英特尔不得不承担了近5亿美元的损失。还有其他各种事故，比如阿丽亚娜5型火箭的爆炸和巴拿马癌症研究所辐射计量超标事故等，实际上都可以通过形式验证得以避免。

硬件系统有许多应用都至关重要，其产生的任何故障都可能导致极大的经济损失或物理损害。 本文将讨论形式验证及其各种技术形式。

目的

形式验证技术可以追踪标准验证技术检测不到的错误。而且，若使用标准技术检测可以检测到错误，那形式验证通常可以以明显更快的速率识别错误。在通过模拟和仿真对设计进行功能验证之前，通常就已执行了形式验证。

形式验证的一些优点如下：
· 在设计周期早期发现bug
· 耗时更少
· 可靠
· 更快
· 更详尽

形式验证技术

下图说明了各种形式验证技术：

图1：形式验证技术（来源：Aijaz Fatima)

模型检查

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

以下步骤说明了模型检查的过程：

1. 对系统进行建模以得到模型M。具体来讲，系统被建模为一组状态，而状态之间具有转换，转换用于描述系统如何响应内部或外部刺激从一种状态变换到另一种状态。
2. 使用属性规范语言（如PSL或SVA）创建要验证的属性，以得到公式ɸ。属性是设计行为的描述。
3. 运行模型检查器以确定模型M是否满足公式ɸ。
4. 如果模型不满足属性，则生成反例。反例是违反属性的刺激，通常用仿真中的波形来表示。
5. 在仿真中使用系统模型运行反例以查找错误位置。

图2：模型检查的程序（来源：Aijaz Fatima）

优点和缺点

一旦将系统模型和属性规范提供给模型检查器，验证过程就将是完全自动的。但是，从模型检查器要处理的状态数来看，模型检查适用于小型系统。

定理证明

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

以下步骤解释了定理证明的过程：
1. 在形式数学逻辑中将系统建模为一组数学定义。
2. 从数学定义中导出系统的属性。
3. 使用定理证明器验证系统是否符合规范。定理证明器也可以称为证明助理。目前有各种可用的定理证明器，根据其基础逻辑进行分类。

图3：定理证明的程序（来源：Aijaz Fatima）

优点和缺点

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

等价性检查

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

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

图4：逻辑等效性检查（来源：Aijaz Fatima）

顺序等价性检查（SEC）：顺序等价性检查是验证两个设计在功能上是否相同的过程，并且在提供相同输入时验证是否有相同的输出。它用于比较两种设计的顺序逻辑，而这两种设计可能有不同的实现。SEC是一个复杂的过程，因此非常受设计规模的限制。

有时，IC的设计会在最后一刻进行修改，以合并一些功能、时序、电源或其他修复，或者包括一些额外的逻辑，如扫描逻辑、电源控制电路等。这些变化也需要验证。标准验证程序会耗费大量时间，因此会推迟产品上市时间。而顺序等效性检查将修改后的设计与标准设计进行比较，并验证它们在功能上是否一致。

图5：顺序等效性检查（来源：Aijaz Fatima）

总结

总而言之，形式验证是一种自动检查方法，可以捕获许多常见的设计错误，并可以发现设计中的歧义之处。它是一种详尽的方法，涵盖了所有输入场景，还可以检测边角案例异常。

形式验证可以节省设计人员的时间和精力，因为潜在问题在开发测试环境之前即被发现。它可用于设计的高级描述、RTL或GLS表示等阶段。市场上有各种各样复杂的形式验证工具，其中许多工具还提供按钮方式用以查找设计中的问题。

本文同步刊登于电子工程专辑杂志2019年7月刊