采用形式验证方法可以更早地发现设计中的缺陷，具有100%的覆盖率，能提高验证质量并降低设计周期和研发成本。通过结合断言验证和仿真验证等方法，可以实现多种方法的优势互补，提高效率。

形式验证的概念由来已久，近两年才开始走上商业化的道路。在2000年的DAC会议上，还只有近5家公司推出自己的形式验证工具，而在2002年DAC会议上，就发展到30多家公司，同时业界标准也开始成形。形式验证及其工具作为功能验证的一个分枝具有其独特的优越，同时又具有新产品早期的不足。现阶段，从应用的角度，主要的任务是如何在此类工具箱完全成熟之前，最大程度的发挥其优越性，弥补其不足，从而达到技术、商业效益的最大化。通过试用多家公司的形式验证工具，特别是@HDL的@verifier，我们总结出形式验证的优点和缺点，在此基础上设计出实际可行的改良流程，并成功应用于项目中。

形式验证的优点

a. 更早发现设计缺陷，降低周期和成本

由于市场竞争激烈，IC设计规模越来越大，而设计周期却越来越短。能否及时发现错误对设计周期有很大的影响。另一方面，根据错误发现的时间和纠正错误所损耗的资源的关系图，错误是否被更早的被发现同样对设计经费有很大的影响。形式验证工具能够根据设计的结构自动地提取特性(property)，表达成作为判断标准的断言(assertion)并且给与验证。由于形式验证的方法不需要验证者给与激励，所以工程师能够在仿真之前较方便的发现一些错误，从而做到最早的纠正设计中的不良。

在应用形式方法之前，我们通常的做法是首先将实现设计功能的代码完成，然后建立测试平台，给与通常的一些激励，确定整个系统是否能够实现基本的一些功能。最后根据特定的测试目的，给与特殊的激励，确定目的是否达到。在此过程中，一直需要人员参与，难以提高效率。应用形式方法，在代码刚刚完成，甚至在仅完成部分代码时即可进入验证。例如，一个系统由A、B、C、D四个模块组成，当A模块完成时，即可应用形式工具验证A模块。由于形式验证主要是通过电脑来完成，在形式验证时，设计人员的大部分时间可以用来编写模块B，以后类推，直到四个模块全部完成，就可进入系统级验证。这种流程可以大大的解放人力，从而提高设计效率。

b. 断言取代测试例(test case)，减小验证难度
利用基于仿真的验证方法，工程师往往为了验证某一特性而编写一系列的测试例，甚至要考虑到一些特殊的测试例。这一切需要花费大量的时间、精力。随着所验证的逻辑的复杂程度的不断加大，验证所需的测试例成级数增长，以至于某些特性已难以用测试例完全验证。对于形式验证，只要能将特性表达成为断言，形式验证工具能够自动验证特性的正确性，极大的方便了测试者。最近，形式验证工具所用的语言已标准化，测试者能够更方便、准确的表达所要验证的特性。

以下面的代码为例：

if(a || b)

;

else if(a)

;

else

;

应用仿真的方法，ab四种可能的激励00，01，10，11都要验证到，最后才发现RTL code2未能进入。当逻辑关系复杂时，采用人工的方法分析其关系使此类问题变得非常困难，分析过程中经常出错。因此，工程师常采用流程图和真值表等方法协助解决问题，而应用形式方法，EDA工具能够帮助工程师迅速发现问题。如上段代码，形式验证工具能自动检测出RTL code2不能进入。

c. 100%覆盖率，提高验证质量
形式验证不再依赖于测试者所给与的激励，而是通过数学的方法验证RTL代码与断言是否一致来确定设计的正确性，从而规避了测试例完整性问题，达到验证的100%覆盖率。例如，为了确定信号load到达后，信号count载入输入信号cin，只要有下面的断言即可，无需再考虑其它条件：

load -> ($next(count) == cin)

d. 结合断言验证方法，快速隔离错误
如今，断言验证的思想方法已广泛应用于ASIC验证中。这主要是由于断言验证能够增强代码的可观测性，迅速找到错误根源。通常，形式验证工具应用断言验证的方法，断言以注释形式出现在代码中，从而既不影响原有代码的工作，又充分发挥了断言验证方法的作用，快速隔离错误。

e. 不影响原有验证流程，易整合其它验证方法
ASIC系统不断增大，以至于任何一种验证方法都难以单独完整地完成验证任务。因此，各ASIC设计公司应用多种验证方法相结合，从而快速、高效完成验证任务。这需要各验证方法能够较好的相结合，图2为形式验证和仿真验证结合应用的框图，图中黄色部分为形式验证，红色部分为仿真验证。可见形式验证能够和仿真验证完美地整合在一起，而互不影响，这有利于多个工作组合作。

形式验证方法的不足

a. 适合模块级或中小系统级的验证
由于形式验证存在状态空间爆炸性增长的可能，当系统变复杂时，验证将占用较多的计算机资源，耗时增加。验证300行，5个断言左右的代码，使用双CPU(933MHz)，3G内存的电脑，约耗时2小时。当系统复杂程度超出状态空间搜索的半径所能覆盖的范围，形式方法已无法完成验证任务。目前，已经有采用能够解决更复杂问题的算法，这种问题已有较大的改善。此外，逻辑锥体优化(Cone Reduction)、等级验证、分散处理等技术的应用，进一步增加了形式方法解决问题的能力。另一方面，形式方法不能完全证明为正确时，则进行部分验证，通过举出反例来协助验证。

b. 适合控制逻辑验证，验证的完整性取决于特性是否被全面准确的表达
形式验证一般具有两种断言：一种是工具自动提取的结构方面特性表达为断言，一种是用户为验证功能方面的特性而应用形式语言定义的断言。一个系统是否被完整的验证取决于两种断言是否准确表达了特性以及特性是否被完全表达。

形式验证与仿真验证

可见形式验证的方法，能够早期发现错误，100%的覆盖，提高验证质量，同时又只适合模块级和控制逻辑的验证。所以现在形式验证与仿真验证结合使用，实现优势互补，而不是一方替代另一方。经过以上分析，我们设计出新的设计验证流程，将两种方法完美结合。图3为一个由三模块组成的系统的设计验证流程。

图中，黄色代表设计部分，绿色代表形式验证部分，蓝色代表仿真验证部分。从图3可以看出，由于利用了形式验证主要依靠电脑完成，这样模块级的控制逻辑验证可以和其它工作同时完成。由于在模块级数字逻辑验证之前，控制逻辑验证已基本完成，大部分错误已排除，数字逻辑验证大大加快。当进入系统级时，一般逻辑极复杂，形式工具难以完成验证，主要通过依靠仿真验证来完成验证任务。如此，在不同的阶段，应用不同的方法，从而充分发挥两者的优势。通过多个项目实践表明，合理应用此流程，项目时间能缩短至原来的三分之二或更多。

设计实例分析

不久前，Be One Lab公司内部一个项目组在设计一块ATM相关芯片(支持UTOPIA第四代接口)时，就实施了形式验证和向量仿真验证结合应用的方案。图4为设计中所发现的缺陷的具体统计资料。

在RTL代码完成后，采用@HDL的@verifier按照设计规则检测(DRC)、自动功能验证(AFV)和用户指定特性(User Properties)测试三步进行了细致的形式验证。在前端验证的初期，借助形式验证工具的支持，耗时8天共发现28个缺陷，其中有些缺陷很难发现，反过来用向量仿真需要很长的时间并且要经过冗长细心的跟踪才能找到根源。随后验证组进行了长时间的向量仿真测试，指定向量和随机向量的测试例的运行，耗时25天共发现14个缺陷。从此项目看出，形势验证适时地运用于设计代码结束与向量仿真开始之间，不但可以节省大量的仿真时间，加快项目的进度，而且可以检测到设计中许多不易发觉的致命错误。在芯片设计日益复杂的今天，应当给予形式验证在整个设计流程更多的关注和重视。

作者：

吴建群

连志斌

荆滔

尹学武

郭山民

Email: Johnson_wu@b1lab.com

天一集成电路设计(深圳)有限公司