形式验证是一种强大的验证方法，可用于发现conner bug，提高验证效率，缩短验证周期。然而，形式验证的完整性或形式验证边界阻碍了行业中形式验证技术的采用。本文介绍了一种方法，通过了解被测设计和系统分析方法，可以限定形式验证边界证明的深度，并使用抽象模型来实现所需的证明边界，进而完成形式验证sign-off。
在上篇（本篇）中我们将简要介绍形式验证应用、sign-off概念、以及形式验证基本模型和形式验证checker。
一、形式验证基本应用
行业中多数验证工作的完结都是基于仿真定义的。良好的度量标准可用于跟踪验证进度，例如bug率（测试平台bug和RTL bug）、覆盖率目标等。基于这些度量标准决定验证工作是否完成。然而，仿真通常不足以验证当今复杂设计的功能正确性。形式验证（模型检验）可以覆盖所有状态转换，那些仿真难以验证的复杂conner通常就交给形式验证了。
形式验证技术通常有以下应用：
- 自动形式检查（也称为super-lint或形式lint）可以检测死代码，违规代码，不跳转的线网/寄存器和状态机死锁。
- 最近一类形式的“应用程序”，针对特定的验证目标，如时钟域交叉验证、时钟门控等效检查、X传播验证等，可以解决特定的验证需求。
- 基于断言的验证可以通过验证局部断言以及证明是否符合标准接口来发现错误。
- 端到端的形式验证可以通过建立参考模型来取代模块级仿真，并证明模块功能的完整性
在所有这些应用中，端到端的形式验证是最难的，但也提供了最大的好处，使形式验证sign-off成为可能。
无论哪种形式验证应用，对于形式工具验证的每个checker，结果都是确定的（所有状态都证明完成）或不确定的（从复位开始的N个周期的证明情况，部分验证状态未达到）。如果我们可以确定在N个周期内观察到所有需要的设计行为，则不确定的有界证明等同于完全证明，与确定的无界限证明效果等同。我们正是要描述这样一种方法，通过分析来限定有界的证明深度，在表征流片合法的sign-off过程中使用这样的证据。
二、验证sign-off
从模块级设计到流片，在芯片设计流程进行中，因设计改动而花费设计成本成指数上升，如下图。“sign-off”表示特定部门（例如时序、功率、功能验证部门）承诺其工作完成的可衡量标准已经到达。
Sign-off这个词的起源是在ASIC客户将网表移交给其ASIC供应商的时候的签字证明，此时，客户已经满足网表的时序和功能要求，并且客户之后需要的任何改变代价是非常昂贵的。现在术语“sign-off”也表示其他部门的承诺，例如功能验证部门，其承诺RTL已被彻底验证，并且与延迟流片导致的丢失市场的机会成本相比，继续验证的对产品的收获已经达到递减的回报点。基于仿真的功能验证的sign-off要求通常包括跟踪各种度量标准，例如发现bug的数量，写入的功能测试的数量与计划的验证列表的数量，以及所实现的代码和功能覆盖目标的百分比。为了从形式验证团队获得类似的sign-off承诺，我们需要量化来自形式工具的“不确定”结果，特别是因为大多数端到端的形式证明很少给出确定性的结论。这将是本文的重点。
三、形式验证使用模型
提供给形式验证工具的输入是：被测设计（DUT）、一组约束、一组checker（或断言）和一组手动写入的抽象模型（当然这个是可选的），其降低了形式搜索的复杂性。
在给定的运行时间中，对于每个checker，形式工具返回三个可能的答案之一：1.（无界）pass或完整的证明，表明保证在整个搜索空间中不存在错误; 2.fail，以及用户可以调试示例跟踪3.不确定结果或有界通过，以及证明深度N。形式验证实现的验证深度通常比通常模拟仿真测试达到的深度小几个数量级。
这里需要说明的一个问题是：如果我在给定设计上实现N个周期的有界证明，我验证了多少设计功能？换句话说，对于给定的设计，我需要进行多少个周期的形式验证才能验证完全？
形式工具从复位状态开始，对设计执行穷举状态空间搜索。图3可见模拟仿真测试搜索的状态空间与通过形式验证搜索的状态空间的对比。
通常对于较小的DUT或简单的checker，该工具可以保证无限的证明，所有可能性都被验证到。另一方面，对于更大的设计或端到端证明，我们面临指数上升的复杂性障碍（图4，深度每增加一层，所耗费时间指数上涨）。在这种情况下，对于给定的运行时，工具只会报告的pass状态是指限定边界内的。
四、形式验证checker
形式验证证明的复杂性和这种验证结果对验证sign-off的有效性很大程度上取决于形式验证的checker的验证范围。不同checker的验证范围变化很大，checker的形式常有局部断言、接口checker以及端到端checker。局部断言最容易，包括写在RTL内的断言以及如用于时钟域交叉（CDC）检查的checker；接口checker用于验证设计是否符合标准或自定义接口协议，如ARM AMBA AXI等，有时也使用形式断言VIP验证。虽然局部断言和接口checker是很有用的，并且可以发现一些难以找到的错误，但这显然不能说明验证的的完成性，无法用于sign-off的依据。为使形式验证成为sign-off的依据，则必须构建端到端checker（图5）。
证明端到端checker的复杂性很重要，我们很少期望无限边界的证明。在没有无限边界证明的情况下，我们要求每个端到端checker达到有界形式验证所需的边界条件。这个要求类似于仿真中的覆盖率。如前所述，如果我们可以确定在N个周期内观察到所有的设计行为，那么不确定的有界证明等效于完全证明。就像模拟仿真中的覆盖率度量一样，这种度量为我们RTL验证完成执行提供了一个可信度。通过使用这种度量，形式验证现在转变为面向目标的方法。基于checker达到的深度和所需的验证边界之间的差异，形式工程师可以决定是否添加抽象模型或增加机器工作量。有了这些指标，依据形式验证结果，决定验证工作sign-off就变成可能。
结束语
由于SoC设计的复杂性，我们基本不会使用形式验证做无边界证明，这样太耗费时间和人力成本了，所以这里提出了先确定一个有效的验证深度或边界，然后对此深度内的所有状态空间进行穷举证明。这种方法对形式验证计划进行可衡量的量化，从而完成形式验证sign-off。关于如何确定有效的验证深度或证明边界，我们会在下篇介绍，同时会讨论如何使用抽象模型实现形式sign-off边界。
谢谢你对路科验证的关注，也欢迎你分享和转发真正的技术价值，你的支持是我们保持前行的动力。
