| 数字芯片设计的断言验证 |
摘要
随着设计规模及其输入数据量指数性增长，模拟时间已长得无法忍受。另外，也很难判断模拟验证的完备性。形式验证不用向量、运用数学方法证明设计的特征和等价性，对这两个问题给出解决办法，但技术发展仍存在不少难题。在模拟中引入形式验证技术，形成的断言验证方法，可能是解决验证危机的有效办法。
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永远不会上溢）；或者一个指定状况永远不会发生（几个独立状态机不会同时产生总线请求）。
使用断言的核心想法是，让设计师把设计假设、意图传递给验证过程，改善了设计师和验证师的沟通。设计师能利用验证知识改善设计流程，而验证师有了精确的设计特征来验证。实际上，当设计师在设计过程中写断言时，进一步明确了假设和特征，因此写出更好的代码。另外，考虑到模块的可验证性，设计师更有可能选择减少系统验证成本的实现方式，从而得到了更易验证更高质量的设计。
设计师通过断言形式地捕获规范、假设和设计的行为特征。以简洁的格式捕获设计意图，从设计流程开始就剔除错误，同时使验证过程自动化。断言捕获接口约束，精确定义符合接口协议的可能行为。模拟时不断检查这些断言，然后形式工具对断言和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时代，芯片上不仅有数字电路，还有模拟及混合信号处理电路。对于模拟和混合处理信号电路的验证，还没有太好的办法，这需要继续研究和探索。
|
|
楼主
标题置顶
标题高亮
