摘要

    随着设计规模及其输入数据量指数性增长，模拟时间已长得无法忍受。另外，也很难判断模拟验证的完备性。形式验证不用向量、运用数学方法证明设计的特征和等价性，对这两个问题给出解决办法，但技术发展仍存在不少难题。在模拟中引入形式验证技术，形成的断言验证方法，可能是解决验证危机的有效办法。

1. 形式验证

    形式验证是一种系统化方法，用穷举的算法技术证明设计实现满足设计规范的特征。它覆盖了输入的所有可能序列，不需要开发测试向量，检查所有的边角逻辑，提供了完整的覆盖率。

    模拟验证中，验证师本人分析设计的特征，找出边角功能。然后分析能够激活特征和边角功能的内部状态与外部输入的组合，开发测试实例。并继续模拟，在设计的边界如输出察看是否检测了该特征。如果没有，就返回去重新开发测试实例，接着模拟检查，如此反复。此外，由于含糊地理解和解释手写规范，许多错误都引入了测试基准，会引入不必要的验证问题。而在形式验证里，只要验证师指定设计特征，由机器应用穷举算法分析设计并进行证明和证伪。验证师摆脱了分析和估算激活特征的状态和输入组合以及输出推理的过程。验证师放弃设计验证的一些细节，把机械性的重复工作交给推理机器完成，专注于分析指定设计特征，并根据分析结果调整约束。显然可以大大提高验证效率。

    形式验证能给出完整覆盖率，应用数学技术分析所有可能的模拟向量，无需逐一模拟，不需要测试实例。但形式验证还不能取代模拟。因为当前的技术只能处理规模不大的设计。

    形式验证主要有两种方法：等价证明和特征检查。

    1.1 等价证明

    证明最终网表和原始的RTL设计的等价一直是个问题。一种方法是放弃RTL模型，只用门级模拟作功能验证。另一种是用相同测试集在RTL和门级作模拟，然后比较两者的输出结果。显然，用模拟来证明等价是不够的。而且两种方式都会引入模拟瓶颈，延缓项目的上市时间。用形式等价证明取代门级模拟，可极大减少验证时间，能提供穷举覆盖率的验证质量。

    等价证明用数学方法证明两个设计的逻辑功能是否等价，确保最后的设计实现的功能与寄存器级设计相同。证明时，一般选用规范作为比较标准。等价证明可用来验证从寄存器级到GDSII版图整个芯片设计实现的功能，实际上，在低抽象层次更加有用。

    当前RTL设计流程中，需要证明等价性的有RTL和RTL、RTL和门级设计、门级和门级以及版图和门级。为了改善性能、降低功耗、缩小面积或者提高可测性，就要改进RTL设计。综合工具和人工干预都有可能引入错误，就要检验综合得到的门级设计实现与可综合RTL设计的一致性。测试插入、扫描链排序、时钟树综合以及模块的自动生成，也都有可能把错误引入门级设计，因此要检查修改前后门级实现的一致性。物理设计工具中的缺陷和人工修改版图，都会引入错误。物理设计实现的验证，首先从版图中提取出门级模型，然后与门级设计进行比较，来证明两者的图形的等价性，即版图和电路一致性检查。

    当前主流RTL设计综合技术只优化组合逻辑，不改变时序逻辑。因此形式等价证明工具假定设计的时序逻辑相同，只证明综合逻辑的等价性。形式等价证明精彩之处在于用符号方式来推理证明或证伪等价性。符号逻辑，在整个输入范围内分析代表逻辑网络的数学表达式，从定义上讲它就是穷举的。因此只要证明表达式等价性，就证明了在任何输入输出上的等价。但等价证明算法非常复杂，无法处理很大的设计。因此必须对设计进行划分以限定问题。一般把设计分割成逻辑锥。逻辑锥是一个逻辑网络，所有的边界都由寄存器、端口或黑盒组成。锥的概念源于这种逻辑网络有多个输入一个输出，呈锥子形状。

    1.2 特征检查

    特征检查用数学方法检查设计是否具有给定的特征，如总线控制器不多于一个或者每个发出的信息包都得到了确认。特征比较小，易描述。特征集可以根据设计的进展添加完善。特征检查多用在业务级和寄存器级，这样可以尽早发现错误，以较小代价修正错误。

    特征是设计的行为属性，可以是高层属性如网络包的收发特点，或低层属性如有限状态机的状态编码特点。特征一般用来描述设计中的边角逻辑、设计边界或内部模块间的接口协议，有时用来描述复杂的RTL构造。

    在形式验证里，不用创建测试基准，验证师用一组特征（称为约束）指定合法的输入行为。这组约束是对设计周围环境的抽象，限制形式引擎在合法状态空间中搜索。约束规定设计周围环境的静态行为，如在写周期里双端口存储器的读地址不能等于写地址；和动态行为，如握手协议中模块收到请求信号后，必须在规定的时间内发出恰当的应答信号。没有约束，形式引擎会报告虚假错误，而非设计错误。事实证明，模拟接口断言/约束对于特征检查很重要。若约束过严，形式引擎就不能发现设计中的错误，也不会给出任何警告信息。对约束进行模拟就可以发现问题，任何在模拟时发生冲突的约束，要么RTL错误，要么约束过严。

    在约束限制下，形式引擎穷举搜索设计的合法空间，证明设计特征永远存在，或找到违反特征的激励序列（反例）。如果既没有发现证明特征成立的证据，也没有特征不成立的反例，该特征就是未定特征。特征检查的首要目的是未定特征的数目最小化，其次是告诉验证师检查每个未定特征的彻底程度。反例很有价值，如果特征描述和约束都正确，那么每个反例都意味着设计中存在一个真正错误。设计师可以根据反例修改设计中对应错误。相反，证据没那么有用，它不告诉你哪儿有问题或者下一步该做什么。只有设计中所有特征都有证据证明其成立，证据才能提高对设计质量的信任程度。但也许有些特征漏掉了。搜寻证据和反例需要不同的技术，即静态形式验证和动态形式验证。

    静态形式验证从设计的复位状态开始，在约束限制下，运用多种算法证明违反某个特征是不可能的。主要的算法基础是模型检查、符号模拟和基于SAT的推导。为了处理大规模设计的复杂特征，需要划分设计，抽出与该特征有关部分进行证明。这种对设计进行划分的形式技术叫做有界模型检查方法。对简单特征或者很小的设计如两万门，静态分析验证不仅能提供证据也能找出反例。

    动态形式验证主要用来搜寻反例即设计错误，而非证据。为了效率最大化，它从设计在模拟时的某个状态（种子）开始，因此是动态的。动态形式验证算法分析每粒种子。给定种子后，依据约束，在种子开始的几个周期内，用极快的有界模型检查方法为每个特征穷举搜寻反例。发现反例后立即报告，并移向下个特征。所有特征证明结束后，移向下粒种子。如此反复。

    围绕种子穷举搜索的深度，以周期数计算，叫做证据半径。对于未定特征，它表示验证的彻底程度，半径越大，验证越彻底。如果用等价模拟周期数衡量，即使小到五个周期的证据半径， 也执行了大量验证。保守起见，假定只有十个输入能影响某特征。因此每个周期有210种可能的激励序列。五个周期的深度就有(210)5个可能的激励序列。显然，不可能用模拟穷举验证该特征。实际上，典型设计中可以影响特征的输入要比十个多得多。

    直观上讲从模拟产生的状态开始搜索应有助于发现错误，事实证明这种方法相当有效。好的模拟能让设计穿越许多边角逻辑情况，其中许多可能是逻辑盲点，只用形式算法就能验证。动态形式验证从这些边角逻辑而不是从复位状态开始，用很小的证据半径就能查到设计错误。

    2. 断言验证

    断言验证就是在模拟中引入形式特征检查的验证方法。用这种方法，设计师编码时插入对特征的描述—断言。代码完成后，进行模拟以检查断言，并修改模拟时断言发现的问题。最后，特征检查根据约束限定，穷举搜索设计的状态空间、证明或证伪断言、查找设计的错误。很多人感觉到，断言验证将是芯片设计业中下一个突破点，使工程师能继续设计和验证更大更复杂的电路。断言验证，给模拟验证的测试基准和监督技术带来许多非常需要的技术手段，也有助于普及和接受正在出现的形式验证技术。

    2.1 断言简介

    断言是对设计应当如何执行行为的描述，是嵌入设计的检查。断言一般用在协议可能误用或者设计意图可能不正确实现的地方，通常是功能划分模糊、模块间接口或者复杂的RTL结构。RTL编码前，把设计划分为多个模块，用断言形式地规定模块级接口协议。如握手协议中，模块收到请求信号后必须适时做出响应，反之断言冲突发生。这些形式接口规范，在模块级特征检查时用作约束模型，模拟时作为监督器。显然，通过断言，在RTL编码前消除了设计师对接口的误解。RTL编码时，为任何功能划分模糊或边角逻辑添加断言（FIFO永远不会上溢）；或者一个指定状况永远不会发生（几个独立状态机不会同时产生总线请求）。

    使用断言的核心想法是，让设计师把设计假设、意图传递给验证过程，改善了设计师和验证师的沟通。设计师能利用验证知识改善设计流程，而验证师有了精确的设计特征来验证。实际上，当设计师在设计过程中写断言时，进一步明确了假设和特征，因此写出更好的代码。另外，考虑到模块的可验证性，设计师更有可能选择减少系统验证成本的实现方式，从而得到了更易验证更高质量的设计。