IP验证的端到端形式化验证策略

摘要：IP验证传统上包括某种形式的受约束的随机验证方法，例如UVM，也可能包括对设计的一部分进行形式化验证。但是，在运行第一个随机测试之前，通常都有一个将所有验证基础架构汇总的提前期，并且覆盖率闭合也很耗时。对设计的一部分进行形式化验证有助于减少UVM测试平台的覆盖空间，但仍需要完整的UVM测试平台基础结构，并且还需要用于形式化验证的其他资源。在本文中，我们将端到端（E2E）形式化方法作为仅使用形式化工具来验证IP的可行选择。我们使用交叉开关（XBar）和中断控制器（INTC）这两个IP来呈现关于我们方法论有效性的经验证据，并将其与使用标准UVM验证的其他IP进行对比。我们还介绍了在这两个模块上部署E2E形式化时遇到的一些挑战，并讨论了克服这些问题的策略。我们还为部署E2E形式化方法提供了一些建议，并得出结论，与基于UVM模拟的方法相比，我们的E2E形式化方法能够提供至少相同的验证质量，同时验证周期显着缩短。

引言

在我们的E2E形式化验证方法中，使用基于IP规范的形式化属性来完整描述IP。使用IPXACT XML文件中自动生成的断言检查寄存器。标准接口使用形式化的特性证明套件而不是通过VIP进行检查。DVE编写新的断言时，将并行完善验证环境和IP，并调试断言的反例。通过与设计团队经常对IP规范进行审查，来检查这些断言的质量和完整性。一旦所有形式化属性均被设计人员批准，并且所有断言和证明工具包均已通过验证，则该IP被视为经过充分验证。

我们之所以选择这种方法，主要是因为我们预测它可以用更少的精力达到与UVM相同或更高的验证质量。E2E形式化验证不承担编写UVM测试平台所带来的开销，例如编写自定义代理，序列库和记分板。还可以在交付RTL之前获得IP规范，从而使DVE可以在开发验证环境方面抢先一步。我们在E2E形式化验证方面的经验表明，与基于模拟的测试平台相比，它还有其他优势，这些将在本文档的后面部分进行深入讨论。

选择用于形式验证的IP时，仔细评估与该方法的兼容性至关重要。通常，IP必须较小且相对简单。我们选择使用我们的方法来验证中断控制器（INTC）和交叉开关（XBar）。

中断控制器

中断控制器负责将设备和软件中断路由到动态位置。它接受不同级别的中断输入，并将它们路由到中断标志寄存器和路由配置寄存器中指定的位，然后在该位置设置中断标志寄存器的位。每个中断标志寄存器都映射到唯一的输出中断，只要将中断标志寄存器设置为非零值，就会产生一个中断。输入和输出中断都可以在配置寄存器中单独屏蔽。可以随时操纵配置寄存器和中断标志寄存器，从而允许软件控制的中断，动态路由和中断屏蔽。

交叉开关

交叉开关是一个仲裁程序，它控制三个不同请求者对共享内存空间的访问。它支持轮询、固定优先级和LFSR优先级方案。它允许单个请求者锁定对bank的独占访问。每个bank模块都负责仲裁逻辑，并且包含了大多数交叉开关的复杂性。

挑战

通常，由于仅使用形式化的验证难以被接受用以取代受约束的随机验证流程。因此，从技术和报告的角度来看，我们在部署E2E形式化方法时都遇到了许多挑战。其中一些描述如下：

质量：对于E2E形式化方法，我们必须确保我们通过编写的所有断言涵盖了设计的所有功能/方面。那时，EDA工具没有很好的覆盖率报告（后文详细讨论），与传统的模拟测试平台相比，我们不得不花额外的时间来检查断言。但是，这并不是工作的重要部分。
验证IP：我们计划为所有标准接口（例如APB，OCP等）和配置寄存器（configuration registes，即CSR）编写断言。开发这些断言需要投入大量的精力。幸运的是，大多数工具供应商都有一些我们可以利用的“证明工具包”（Proof-kits）。这些工具包类似于模拟测试平台中的VIP。但是，并非所有工具供应商都具有相同功能的形式证明工具。在某些情况下，还需要其它胶合逻辑来整合成证明套件和/或其他配置选项。
收敛：对于INTC，由于微体系结构的对称性，我们选择将断言的生成模板化。这导致为E2E形式化验证生成了420K大小的断言，并且我们很快遇到了几个工具上的问题。这些问题不限于任何特定的EDA供应商。存在两个主要的基本问题：
1. 编译时间：甚至在开始证明之前，都需要花费难以接受的大量时间来编译断言。将420K的断言拆分为多个较小的10K-40K文件块后仍需要近几个小时的编译时间。我们必须与客服紧密合作来调试问题，最终通过工具的R＆D更新/补丁将编译时间减少到合理的数量。
2. 证明时间：解决了编译时间问题后，我们很快遇到了非线性运行时增长与断言数量之间的关系。考虑到有限的许可证和计算资源，到目前为止，我们仅能并行处理INTC证明。为了进一步解决验证时间，我们必须部署后续讨论的策略。
报告：在开发时，可用的形式化工具并未提供与模拟覆盖率指标（例如代码覆盖率）进行轻易比较的覆盖率指标。这需要额外的精力来开发脚本，把我们拥有的指标重新格式化，使其成为更传统的格式，使工程师、程序和高管者更容易理解。由于没有一种格式可以与仿真报告进行对等的比较，我们在验证质量和进度方面不断的面临挑战，并且不得不经常深入研究E2E形式验证结果的细节。在许多情况下，我们必须与工具供应商紧密合作，以设计出对形式化验证报告进行后期处理的方法。

策略

分而治之

某些IP（例如中断控制器）特别容易受到有关断言个数导致的非线性运行时间增长的影响。通过限制每次执行的断言数量，有效地将断言的总集合分成较小的组，从而减轻了这种过多的运行时间。即使在按顺序执行这些划分后的断言主体时，总的运行时仍显示出接近线性模式的增长模式，这与玩增证明中看到的非线性增长相反。对于中断控制器，此差异使运行时间减少了25％，并且断言的数量越多，差距就越大。

分层策略

IP通常会将同一子模块用相同的参数实例化多次。在这种情况下，高效的方法是将子模块验证一次，并在顶层验证多个实例的集成。这减少了验证IP所需的断言数量，大大减少了运行时间，但保持了相同水平的验证质量。

例如，交叉开关中的每个存储库都包含其自己的特定子模块的实例，该子模块负责优先级逻辑和选择标准。检查此功能对于交叉开关的验证至关重要，但是没有必要在相同实例中都对优先级逻辑部分执行相同的检查。这些子模块集的集成测试是在顶层进行连接并检查的。

通过允许DVE在子模块级别上开发，诊断和调试测试平台，该方法降低了断言复杂度并加快了调试时间。与UVM相比，它还具有优势，因为与基于仿真的方法相比，使用E2E形式化方法实现子模块级验证所需的工作量更少。在UVM中，如果不为子模块开发单独的测试平台，则很难进行子模块级别的验证。然而，在E2E形式化方法中，只需为子模块编写断言即可执行类似的检查，这些断言可以在测试平台的顶层轻松导入。

抽象化

抽象化是识别IP或测试平台中的模式，并通过更高级别的抽象以更简单的术语描述模式的过程。从细粒度到较宽粒度的这种转变可以减少所需的断言数量，从而带来性能优势。

事实证明，抽象化对于减少中断控制器中的证明时间非常有用。该IP接受由上升沿触发的中断线程。验证这种边缘检测功能的简单方法是为每条中断线程写一个断言。但是，由于$ rose（）这类的系统功能只能在单个比特位上运行，因此只能在比特位级别的粒度下才可以不应用抽象化。相反，在一个断言中将所有中断线程都视为一个比特位向量的情况下，在所有中断线程上测试相同的功能将更加简单。这是通过将边缘检测器逻辑引入到胶合逻辑中，然后在重写断言边缘检测检查时利用这些结构来实现的，从而使它们以字粒度级别进行测试。这种粒度上的变化使中断控制器的边沿中断检查的断言计数减少了32倍。

此方法提供的优点是，它可以显着减少断言计数，而不必丢失任何功能验证。如果存在不需要验证的功能（例如馈入多路复用器的数据位的各种可能值），则可以减少更多。但是，与分层策略和黑匣子一样，必须格外小心，以确保不排除未经验证的功能。

常规方法

我们的方法中还利用了一些传统的形式化验证策略。尽管在E2E形式化验证中进行详尽测试非常重要，但经过仔细考虑，如果不更改IP的功能，则可以安全地排除或限制组件。例如，在仅测试总线连接性的情况下，无需测试总线的所有可能的数据或地址值。可以将这些信号约束为不随机化以减少运行时间。其他传统方法，例如利用并行性和执行工具特定的优化，也被用来减少运行时间。

结果

我们比较了基于传统仿真（UVM）的环境与E2E形式化验证之间的各种指标，以分析E2E形式化验证方法的质量和投资回报率（Return on Investment，ROI）。为了规范通过不同方法验证的各种IP的复杂性，我们将门数视为比较分析的一个很好的一阶近似值。然后，我们根据资源、时间表、测试台代码行（lines-of-code，LOC）和逃避这些IP测试台的错误来考虑验证每个门所需的工作，以评估每个测试台的相对效率和质量。最后，我们比较了模拟验证和E2E形式化验证测试平台之间的效率。

下表突出展现了各种测试平台的一些关键指标。所有数据均来自最近已流片的项目。

选择了多个IP，其中包括图像处理，信号处理和通用控制密集块；
门数不包括任何内存，但代表IP中的组合+顺序逻辑总数；
持续时间仅是工作日（即星期一至星期五）；
DV（Design Verfication）代码行在测试平台中不包括空白或注释代码，但包括所有UVM组件，序列，断言，测试用例，覆盖结构等。其中不包括第三方VIP代码；
逃脱Bug是在IP的RTL代码冻结后逃脱IP验证并在更高级别的测试台上捕获的RTL Bug的数量；
Bug密度是每一千行DV代码行发现的RTL Bug总数；
假定许可权和计算资源可用，不作为比较的因素。
UVM DV资源是具有丰富的经验组合，范围从1-10年的从事受约束的随机验证到1-7年的UVM / OVM方法学。E2E形式化的DV资源具有SVA和大约1年的形式化验证经验。

关于数据的其他注释如下：

每个LOC每个工作日验证的平均门数约为0.09，IP1 由于IP1是一个异常，因此不考虑入内。由于IP的微体系结构占用了大量寄存器文件。如果考虑IP1，则平均值为0.16；
对于INTC，总LOC-DV还包括使用模板生成声明所需的代码/脚本；
IP9有较多的逃逸错误主要由于所有权的流失，在整个IP开发过程中，该模块归几位不同的设计师所有。

我们选择了三个指标来比较UVM和形式化的E2E方法之间的质量和ROI：

每天每个LOC-DV验证的门数（即DV效率）
每个一千个LOC-DV的错误密度（即DV质量）
从IP测试平台逃逸的Bug

基于上述标准，我们得出以下推论：

与模拟或UVM的测试平台相比，使用形式化的E2E可以达到相同甚至更高的效率。
在错误密度方面，形式化的E2E在每个LOC-DV中可以比UVM测试平台发现更多的错误，这主要是由于我们只需要声明和形式化测试平台所需的最小胶合逻辑（如果有）。我们也不需要开发任何UVM / VIP组件。
就错误逃逸而言，E2E形式化测试平台可以达到与UVM测试平台相同的IP验证质量。
即使我们花了额外的时间来审查E2E形式化方法中的断言，也可以通过以下方式来节省时间：
1. 测试平台编码：与UVM测试平台相比，所需的代码更少，并且测试平台在RTL交付的第一天就可以使用了。最早的RTL错误可以在第一个RTL版本发布后立即发现；
2. 覆盖率闭合：证明是详尽无遗的，因此没有覆盖率闭合的步骤；
3. 回归：由于详尽无遗的证明，因此不需要随机测试和夜间回归；
4. 错误重现：这很简单，调试可以立即开始，而无需等待仿真重新运行失败的测试。
我们发现重复的模式，对称性和可重复使用的子块使我们能够使用前面描述的策略简化测试平台，从而节省了时间运行时而不必牺牲验证质量

总体而言，我们发现E2E形式验证相对于UVM具有令人信服的成本优势，同时实现了与模拟/ UVM测试平台相比至少相同，甚至更好的验证质量。

未来的工作

我们在E2E正式验证方面的经验揭示了我们认为仍有改进空间的几个方面。它们如下：

覆盖率报告：在中断控制器和交叉开关的DV周期中，可用的覆盖率报告解决方案功能有限，并且与基于模拟验证的覆盖率报告不能很好地比较。具有易于与基于模拟验证的覆盖率报告进行比较的覆盖率报告，将使E2E形式化验证从管理角度更易于被接受。
工具辅助的IP评估：可以使用工具（可报告有关E2E形式验证适用性的IP信息）来增强E2E形式验证候选对象的选择过程。访问关键数据点，例如最大逻辑锥深度，重复的子模块计数和门计数，使DVE可以更好地理解该模块的复杂性，并有助于引导他们对IP的适用性进行合理的判断。进行E2E形式化验证。
集成的运行时间的减少：上述某些策略可以部分或全部自动化。下一代的形式化工具可以在“分而治之”方法中增加对对断言进行分组的支持，并可以确定何时某个模块将特别适合于“分层”策略。将这些功能预先集成到现有的形式化工具中，并利用我们的方法减轻DVE的工作量，从而加快流片进度。
证明工具：证明工具通过分担验证标准接口的工作来加快流片进程，这与基于模拟验证中的VIP十分相似。随着更多可用的证明工具，更多IP可以使用E2E形式化验证。

部署E2E形式化验证的建议

IP选择：并非所有IP都非常适合E2E形式验证。在考虑此方法时，至关重要的是仔细选择与该方法兼容的IP。通常，我们推荐在SVA中可以完全指定的IP，这些都是E2E验证的优先选项。更具体地说，此方法的理想候选者应具有较浅的逻辑锥度，较低的门数和较低的复杂度。
增强断言质量：在我们进行研究时，现有的形式化工具并未提供类似于基于模拟指标的覆盖率跟踪解决方案。如果没有覆盖率解决方案，则必须在DE和DVE之间进行广泛的审查，以增强测试台的质量。评审应检查所有功能均具有显式检查；在未指定行为的情况下检查应失败；在任何定义的行为之前没有明确定义的触发器，并且所有约束不排除与IP的任何合法且有意义的交互，否则失败。但是，当有形式化的验证覆盖解决方案可用时，我们强烈建议将覆盖率跟踪与测试台审查配对。
上述策略：我们还建议在部署适用于这些策略的IP上的E2E形式验证时，采用上述策略。使用这些策略可以减少断言计数和运行时间，而不会影响验证的质量。

结论

我们发现端到端形式验证非常适合某些类型的高度对称且控制路径密集的设计。与传统的基于UVM的方法相比，我们的方法能够节省验证投入和资源，并且能够达到与传统UVM测试平台至少相同的验证质量。

原文来自：DVCon2017_USA, 点击阅读原文去路科官网下载DVCon2017论文合集，还有更多资料等你来哦！