深层解析形式验证

　　形式验证（Formal Verification）是一种IC设计的验证方法，它的主要思想是通过使用形式证明的方式来验证一个设计的功能是否正确。形式验证可以分为三大类：等价性检查（Equivalence Checking）、形式模型检查（Formal Model Checking）（也被称作特性检查）和定理证明(Theory Prover) 。

　　等价性检查的验证用于验证RTL设计与门级网表、门级网表与门级网表是否一致。在进行扫描链重排、时钟树综合等过程中，都可以用等价性检查保证网表的一致性。等价性检查已经融入IC标准设计流程中。等价性检查在检查ECO时非常有用。例如，设计者在修改门级网表时，由于手误，错将一个或门写成或非门，等价性检查工具通过比较RTL设计与门级网表，可以很容易地发现这种错误。

　　模型检查用时态逻辑来描述规范，通过有效的搜索方法来检查给定的系统是否满足规范。模型检查是目前研究的热点，但其验证的电路规模受限制这一问题还没有得到很好的解决。

　　定理证明把系统与规范都表示成数学逻辑公式，从公理出发寻求描述。定理证明验证的电路模型不受限制，但需要使用者的人工干预和较多的背景知识。

在当前复杂的数字设计开发过程中，功能验证十分重要。虽然硬件的复杂度仍遵循摩尔定律持续增长，但是验证的复杂性更具挑战。事实上，随着硬件复杂性随时间呈双指数增长，验证复杂性理论上也呈指数增长。验证已被公认为是设计过程中的主要瓶颈：高达70%的设计开发时间和资源花在功能验证上。Collett International Research认为，即使在验证上花费如此巨大的精力和资源，功能性缺陷仍是芯片重新流片的头号原因。

　　功能性验证挑战

　　边际情形(corner-case)的缺陷是仿真伪像，由于以仿真为基础的验证具有非穷尽的固有特性，因此边际情形无法被检测到。事实上，不管你用多少时间仿真，也不管你的测试平台和发生器有多么智能，通过仿真验证设计意图对于最小电路以外的所有电路来说都是不完整的。基本的仿真伪像可以被分成三类：穷尽型、可控型和可观察型，如下表1所示。

　　形式验证是一个系统性的过程，将使用数学推理来验证设计意图(指标)在实现(RTL)中是否得以贯彻。形式验证可以克服所有3种仿真挑战(表1)，因为形式验证能够从算法上穷尽检查所有随时间可能变化的输入值。换句话说，没有必要表明如何激励设计或创建多种条件来实现较高的可观察性。

　　虽然从理论上讲，仿真测试平台的输入端口针对待验证设计(DUV)具有较高的可控性，但测试平台对内部点的可控性一般较差。为了使用基于仿真的方法识别设计错误，以下条件必须保持：

　　* 必须产生正确的输入激励，以激活(也就是敏感化)设计中某个点的缺陷

　　* 必须产生正确的输入激励，以便将源自缺陷的所有效果传送到输出端口

　　在使用基于仿真的验证时，需要规划设计中需要验证的对象：

　　* 定义需要测试的各种输入条件

　　* 创建功能性覆盖模型(确定是否做了足够的仿真)

　　* 搭建测试平台(检查器，测试桩，发生器等)

　　* 创建特定的直接测试

　　* 成年累月的仿真

　　现实中，工程师一直在反复做着这些事：运行测试、调试故障、再次仿真回归组、观察各种覆盖率指标，以及调整激励(例如操控输入发生器)以覆盖以前未覆盖的设计部分。

　　这里我们讨论一个弹性缓存例子(见图1)。数据可以在时钟域间改变，能够根据两个时钟之间的相位和频率偏移做出调整。数据必须无损地通过弹性缓存进行传送，即使在设计允许时钟不完全同步的情况下。在这个案例中的一个功能性缺陷例子是在时钟有效沿对齐时由于数据的变化而出现的缓存溢出。这就可能要求对所有可能的输入条件进行大量的仿真和考虑，以建模和仿真这种错误行为。

　　

　　图1：弹性缓存框图

　　高层要求

　　许多公司已经采用基于断言的验证(ABV)技术来缩短验证时间，同时改进他们的整体验证工作。然而，一般采用的ABV专注于局部的、在仿真中使用的RTL实现相关断言。所有内部断言的汇聚不会表征或完整规定微架构定义的那种模块的端到端行为。此外，当设计实现改变时，这些局部性断言不能重复使用。换句话说，通过端到端属性(包括数据完整性和包顺序)和规定模块必需的黑箱行为，高层断言(我们在本文中指高层要求)提供高得多的设计功能覆盖率，并且能在各种设计实现和多个项目之间重复使用。更重要的是，通过形式性验证模块的高层要求集，可以使验证完整性和产能得到显著提高。因此，高层形式验证无需模块级仿真，可极大地缩短系统级验证时间。让我们详细地看看图2所示的高层要求。

　　

　　图2：要求与RTL断言对比。

　　Y轴代表抽取层，X轴代表被某个特殊断言或要求覆盖的设计数量。沿Y轴越往上走，被高层要求覆盖的设计空间就越大。证实这些高层要求具有很高价值，原因有很多：

　　1. 高层要求关系到微架构中的要求

　　2. 高层要求关系到测试平台中的输出检查器组

　　3. 高层要求覆盖了与工程师想要写入的数百条较低层断言相同的设计空间

　　4. 高层要求覆盖了由于工程师遗漏的较低层断言的缺失而未被覆盖的设计空间

　　最后一点我们这里举个例子，假如设计包含一个FIFO，并且工程师忘了编写一个断言来检查FIF从不下溢。这种安全性违例将由高层要求加以识别。然而，通过形式性地验证高层要求，高层要求违例的根源就能得以跟踪。例如，如果针对高层要求在影响锥中包含了FIFO，那么导致高层要求不能满足的下溢条件将被检测到。

　　理想的形式验证工具要求具有一定的规模，以便穷尽地检查所有可能的输入条件以及设计中任意点的可控性和可视性(见表1)。我们的旗舰产品，例如JasperGold，就采用了高性能和大规模的形式验证技术，能够穷尽地验证模块是否满足源自微架构的高层要求。这款产品使用数学算法，因为不需要使用仿真测试平台或激励。

　　

　　表1：仿真与形式验证的比较

　　本文小结

　　形式验证要求你以不同的方式思考。例如，仿真是完全经验主义的做法，也就是说，你通过反复试验试图查明缺陷，这要花相当多的时间尝试所有可能的组合，因此永远不会完整。另外，由于工程师必须定义和产生大量输入条件，他们的工作重点将是如何在非设计目标基础上分解设计。另一方面，形式验证是穷尽式数学技术，允许工程师仅关注设计意图，或“什么是设计的正确行为?”。

　　验证实现工作包括将多种输入条件定义为测试计划的一部分、创建功能覆盖模型、开发测试平台、创建输入激励发生器、编写指导性测试以及执行测试、分析覆盖率指标、调整激励发生器以面向未验证的设计部分，然后反复这一过程。纯形式验证技术则相反，专注于证实模块的端到端、直接对应微架构规范的高层要求，帮助用户戏极大提高项目的设计和验证产能，同时确保正确性。