设计师通过断言形式地捕获规范、假设和设计的行为特征。以简洁的格式捕获设计意图，从设计流程开始就剔除错误，同时使验证过程自动化。断言捕获接口约束，精确定义符合接口协议的可能行为。模拟时不断检查这些断言，然后形式工具对断言和RTL设计一起进行分析，搜索设计特征的反例。

    验证方法的核心是一个集成工具组，包括模拟、覆盖率、约束驱动的测试生成和形式分析，该工具组为RTL设计实现提供详细验证。断言从使用角度把这些能力结合到一起。断言用来监督模拟行为、驱动形式验证、控制激励生成，为全面的功能覆盖率尺度打下基础。断言验证在可验证设计中关键作用如图1所示。

    很好的RTL编程习惯。注释好的代码易于维护、理解预期功能，但断言的价值远不止于此。断言更进一步，准确地记录代码预期行为。这种记录方式便于工具验证，而非人阅读注释并试图理解代码是否正确工作。

    断言比纸面测试计划好。断言帮助测试实例自动运行：检验测试实例覆盖了特征并把该实例加入测试集。不用断言就无法保证设计进展时测试实例还能检查预期特征。同时断言提供了一种机制，来测量功能覆盖率和量化测试结果。

    断言易化调试、减少模拟时间。减少调试时间是运用断言的主要动力之一。断言是一种白盒验证技术，提高了被验证芯片的可观性和可控性。一旦设计错误发生，断言能立即探测到，无需等待错误结果传递到设计边界，也就没必要查找和定位错误，这可以省掉好几个小时。致命错误发生后，断言可以终止错误、节省模拟时间。

    断言验证模块间的接口。系统集成阶段，断言作为模块边界的看门狗，确保每个模块服从定好的协议。测试实例根据设计边界观测到的数据判断结果，即使设计内部有协议冲突，也极有可能通过测试。但断言可以帮助消灭这种情况。

    2.2 断言的定义方式

    有四种定义断言的方式：开发验证库定义宣言性断言，Verilog断言构造定义过程性断言，还可用形式特征语言或伪注释指示定义。

    宣称性断言

    最常用的断言定义方法是开放验证库OVL提供的宣称性断言。OVL是基于Verilog的开放源码的断言监督元件库，以相同方式在RTL中定义静态和动态断言；提供统一的消息报告机制；易于定制；提供一致安全级别，发生严重错误时可停止模拟。由于源码开放，能够根据应用进行定制，因此OVL很吸引人。OVL使用断言模块库，因此在设计中必须实例化断言。目前它还无法定义过程性断言。

    过程性断言

    与实例化断言模块相比，用过程性语句定义断言有时更方便。过程性断言在Verilog的always模块中非常有用。RTL编码时，宣称性和过程性断言都是很好的捕获设计意图的方式。如果在这个阶段没有定义断言，有关设计意图的知识就有可能流失，因为不可能有人返回来插入这些断言。

    形式特征语言

    形式特征语言目的在于：用最少的代价指定设计的特征。

    它们擅长创建复杂的时变表达式，通过使用规则表达式，用很少的代码指定复杂行为。已经存在许多年，但仍未进入主流设计，如Sugar，OVA。在设计的所有层次及项目各个阶段，形式特征语言都很有用。系统工程师能用其指定设计的高级特征。这些高级特征断言可用于基于IP的SoC设计验证，无需验证工程师理解设计的细节；RTL设计师可根据它们定义设计的低级特征。与过程性断言相比，形式特征语言更通用，没有针对任何特定的语言。目前用形式特征语言描述断言的工具把定义好的断言放在单独文件，这样形式工具和模拟器能够单独处理。

    伪注释命令

    伪注释把断言埋在注释中，不干扰Verilog语法，不用对模拟器进行任何修改。形式验证工具用专门的语法分析程序读取注释。并为每个断言产生等价 RTL描述， 便于用标准逻辑模拟器模拟。这非常有用，因为它在模拟时自动收集断言覆盖率、创建设计逻辑活动的数据库，并以简洁的方式展现这些活动。

    2.3 仍需完善的方面

    成功应用断言验证，仍需下列技术改善成熟：模拟引擎、分析引擎、断言能力、统一语言。

    模拟引擎直接执行断言检查

    断言是关于设计要素如信号、寄存器、业务等的描述。模拟时检查断言需要存取这些要素，多数情况下每周期都要存取。为了保证足够的模拟吞吐量，就要最小化存取开销。但现在使用PLI监督成百上千的断言，大大降低模拟性能。为了最小化存取开销，要求模拟引擎能直接检查断言。

    多个形式引擎且与模拟引擎紧密结合

    设计的断言类型各异、难易并存，不可能用单个形式引擎证明搜索。应当有多个形式引擎用于形式分析，提高特征检查效率。为了形式分析效率最大化，形式分析引擎和模拟引擎要紧密配合，有效探索设计的状态空间。尤其是，能够生成并证实能引起某个特征或假设冲突的激励，在调试设计错误时非常必要。另外，形式分析需要大容量来发现大规模设计的错误，大容量指设计规模和用状态深度表示的特征复杂度。集成多个形式引擎和模拟引擎，可以有效搜寻复杂设计的边角逻辑错误。

    断言的综合能力

    以前，仿真的唯一价值是性能。不像模拟，仿真不能让测试基准和监督器监测报告仿真器中的逻辑活动。但现在断言改变了这种情况。利用软硬件有效实现的断言，能在保持仿真性能的同时，提供可观察性、改善仿真的调试能力。但在仿真中运用断言的前提是断言是可综合的。把断言写进设计并综合到FPGA，提高了设计的可观察性，使设计师能够监测结果，一旦有断言冲突就报告。因此当设计放置在快速运行的仿真环境中，就能大大帮助设计师找出设计中残留错误。

    统一设计和验证的语言

    正如HDL搭起芯片设计从图形输入到综合的桥梁，解决了设计代沟一样；语言开发对于跨越验证代沟，解决验证危机也非常关键。同样，也需要统一设计和验证的语言来描述今天复杂的设计和测试基准。要求该语言能支持断言描述、高级数据类型、面向对象、并发控制、设计的可观察性、约束性驱动生成和功能覆盖率。把测试基准和断言作为统一语言的一部分，使它们彼此一致，在整个验证中共享通用的语义。这便于模拟引擎直接执行断言检查和形式引擎与模拟引擎的紧密结合。集成环境便于设计师调试设计和断言，也便于采集代码覆盖率和功能覆盖率。采用高级数据类型、并发控制以及面向对象的特性，可提升设计的抽象层次，用更少的代码描述更复杂的可综合设计。另外，面向对象的编程技术比如类、多态性和继承，可以使测试基准逐步集成，以清晰的方式扩展完善。统一的语言描述设计、断言、测试，确保简洁一致的规范、设计和验证描述。

    3. 结语

    芯片产业中出现过两次代沟，设计代沟和验证代沟。设计代沟反映了设计能力和制造能力的落差，通过设计层次上提到寄存器级，HDL和逻辑综合技术大大地改善了设计自动化，成功地赶上了工艺进步。目前面临的是验证代沟，即验证能力和设计能力的落差。

    正如设计复用正在帮助缩小设计差距一样，验证复用能够帮助解决验证危机。 在设计早期，模块不仅包括设计内容，还应包括一整套的输入生成器、输出检验器和覆盖率工具。测试集应当设计成可移植的，不仅在同一设计的不同抽象层次可移植，还可移植到不同设计中便于模块复用。测试集合应该是层次化的，这样当模块集成到系统级设计时，更高级别的生成器和检验器可用于系统级验证。

    形式验证另辟蹊径，用数学方法证明设计特征和等价性。但形式验证算法非常复杂，目前只适合于解决较小规模的设计。断言验证，用模拟把一个大规模设计划分成多个小规模问题，然后由形式验证工具一一击破，是目前最好的方法。

    但芯片设计已进入SoC时代，芯片上不仅有数字电路，还有模拟及混合信号处理电路。对于模拟和混合处理信号电路的验证，还没有太好的办法，这需要继续研究和探索。