如何在数字IP设计中节省时间

众所周知，验证任务在数字IP的设计以及SoC的设计中占有重要地位。 RTL代码和功能覆盖率的目标是达到100％，从而最大限度地缩短获得它的时间。最广泛使用的方法是基于通用验证方法（UVM）随机约束测试（系统Verilog或 e 语言），允许在相对短的时间内构建复杂的测试，同时强调RTL代码和跟踪功能覆盖。一些验证工程师还使用正式的方法来验证块的专用部分，例如标准接口，从而完成IP的验证。

本文将介绍基于正式方法的数字IP验证的不同方法，通过定义属性详尽地验证功能。正式方法具有避免开发测试台的优点。这一新流程已在数字IP设计过程中使用，并已证明可显着缩短验证时间。

通用验证流程

目前，用于验证数字IP和片上系统（SoC）的最常用流程是基于UVM，通过使用第三方提供的验证组件（VC）或非标准时从头开发使用协议。然后用记分板完成测试平台以进行自我数据检查，断言用于验证设计的特定部分，覆盖用于跟踪功能覆盖。在过去几年中，正式验证已经开始用于SoC和IP的验证流程。在SoC中，形式验证在SoC外围设备和焊盘之间的连接验证中变得非常普遍，主要是当多路复用方案由连接到减少数量的焊盘的多个外围设备形成时，这增加了需要验证的组合。有时，在IP验证中，正式方法用于检查总线协议接口和寄存器访问策略。

现在，关注数字IP的验证，我们可以总结如图所示的流程1.当第一版RTL准备就绪时，良好验证流程的第一步从验证和测试计划的定义开始。在这个阶段，我们将定义我们想要检查的功能和测试的框架。

下一步是开发UVM测试台;自定义UVM块用于检查特定的IP功能，而第三方UVM VC则实例化并绑定在RTL上。

此时，我们可以根据验证计划开发UVM测试。每个验证工程师需要牢记的第一件事是测试必须是自我检查;必须使用记分板，检查器和断言自动检查验证计划中列出的任何点。然后，广泛使用覆盖结构可以量化测试的好坏。

图1：数字IP的通用验证流程

有时，此流程可能包括形式验证。在任务的某个阶段，有人可能决定通过使用基于断言的验证IP（ABVIP）和通过编写断言通过有限状态机（FSM）实现的精确功能来检查IP的特定块，例如总线协议接口。

我们知道，验证任务是一个迭代过程，有两个主要的环回：

RTL错误修复

功能和代码覆盖

每当我们发现功能规范与IP行为不匹配时，我们就会向设计人员发出可能的错误信号。这意味着需要修改RTL并发布新的固定版本。现在，进行回归自检测试（即使最初是部分测试）也是一个关键点，它允许我们验证RTL代码没有回归，当然，错误已经修复。这种环回也可以来自形式验证。

当开发了足够数量的测试时，测量功能和代码覆盖率是一个很好的做法。像往常一样，功能和代码的目标是100％，但我们必须考虑到达它的时间。如果我们想要最小化时间，同时保持100％的目标，我们必须改进验证的方法和流程。来自正式世界的一个好建议是代码不可达性分析，它有助于发现无法访问的RTL部分，并且可以从整体代码覆盖率中删除。

一个好的经验法则：'如果我没有运用代码的一部分，很可能是那里存在错误。'因此，我们花了很多时间才能刺激未覆盖的代码，但知道某个部分无法访问可以让我们节省时间和精力。

接下来，我们将描述一个新的流程，其主要目标是缩短用于验证数字IP的时间。保持覆盖目标。

新的验证流程

正式方法是一种详尽的验证，当它是适用时，它使人们能够在更短的时间内和每种可能的条件下检查块的功能。对于常见的动态模拟，这有时是不可行的。

目前，有几种工具可以链接到正式引擎，这些工具已经足够成熟，可以使图1所示的验证流程变为如图2所示的内容。 。

主要的变化是将形式验证作为流程的第一步。真正的第一个检查是对死代码和未初始化寄存器的分析。这是一项零工作任务，因为不需要额外的代码，并且它只需要使用Formal工具编译RTL。随后的反馈可能非常有用，因为它可以让我们彻底清理RTL代码，突出显示从未到过的部分，以及列出可能导致'X'传播的未初始化触发器

毫无疑问，通过使用专用的基于断言的VIP（ABVIP），可以在短时间内完全验证诸如微处理器总线接口之类的标准协议。 Formal流的这些验证组件基于描述协议的断言。验证工程师将专注于失败属性的调试，而无需花时间在测试平台和房地产开发上。通过使用UVM流，我们可以在几天而不是几周内完全验证接口。

可以通过编写自定义属性来验证IP的特定块，以验证已实现的功能。可以使用新的选项，例如引入具有与UVM 记分板相同的众所周知的概念的Formal 记分板，但是利用了Formal引擎的强大功能。它可用于验证FIFO，通常用于处理数据路径流但不是算术数据路径的每个块（例如加法器，乘法器）。

如今，主要的EDA公司制作了基于Formal流程的工具，这些工具使用时髦的技术词汇：'APP'。这个概念是为“特定功能”的调试提供“随时可用”的环境。这些APP自动生成断言，并允许验证工程师专注于调试RTL。

最有用的APP之一是用于验证配置寄存器的访问策略的APP。通过Formal流程，我们可以详尽地验证所有寄存器，尤其是最难验证的状态位，因为它们通常取决于HW状态或特殊输入条件。通常，流程基于IPXACT，然后也可以在设计开发的其他步骤中重复使用。此外，在这种情况下，这种验证可以节省很多时间相对于'经典'UVM随机约束方法。

图2：新数字IP的验证流程

可用APP的数量正在快速增长，这将允许将验证任务从动态移动到静态，从而改善覆盖范围并缩短验证时间。当然，正式流程有一些局限性，目前无法用于验证所有内容;当要分析的状态数（即“形式复杂性指数”）太大时，引擎无法收敛并彻底分析代码。这是一项挑战，可以通过引入新算法和计算能力在不久的将来克服这一挑战。无论如何，我们不能声称正式流程将超过动态模拟，原因很简单：使用'假设'语句会引入隐藏错误的风险，如果属性成功，则有可能如果在实际应用程序中未满足假设条件，则RTL行为将是错误的。这完全类似于静态时序分析（STA）和门级仿真：如果时序约束错误，STA表示设计中没有时序违规，但最终设计不适用于某些极端情况。动态模拟允许我们验证形式'假设'语句以及STA约束。

由于这些原因，验证流程的下一步需要进行UVM模拟，提升通过正式步骤中成功的属性断言，现在也可以在动态模拟中重复使用。在这个新流程中开发的测试数量将少于使用图1所示流程开发的测试数量，因为我们可以专注于正式流程中发现的部分，并为使用它分析的部分开发有限的测试。

图2所示流程的最后几个步骤基本相同：我们运行不可达性分析以删除无法访问的代码，然后分析代码和功能覆盖。

结论

使用形式验证方法作为流程的第一步，代表了一种不同的方法，可以更好地利用正式的好处和有效性：零时间用于构建测试平台和RTL的详尽验证。此外，使用这种方法的学习曲线比UVM更快;用于编写断言的语言是紧凑的（PSL或SVA）并且易于使用。最困难的工作是用人类语言定义最能描述我们想要证明的功能的正确属性。转换为SVA或PSL变得简单易行。

在RTL验证的早期阶段使用形式化方法的主要优点是使用更清晰的代码进入动态模拟，其中许多功能已经过彻底验证并且修复了一些错误。由于正式方法允许我们缩短在验证功能上花费的时间，因此可以大大缩短整体验证时间。