日志

形式验证sign-off(下)

已有 2557 次阅读| 2017-7-30 13:30 |个人分类:验证前沿资讯|系统分类:硬件设计

前面上篇中我们简要地介绍了形式验证应用、sign-off概念、以及形式验证基本模型和形式验证checker。在本篇我们会介绍用于计算sign-off所需证明边界的方法、讨论如何使用抽象模型实现形式sign-off。

一.确定需要的证明边界

我们使用以下步骤确定所需的证明边界：

设计的延时分析
微体系结构分析
涵盖有意义的conner
形式验证覆盖率
形式验证期间看到的fuilure
辅助分析

前三个步骤在形式验证工作的初始阶段执行，而最后三个步骤执在形式验证项目中执行

1.延时分析

这涉及分析从设计的输入到相关输出端口的延时。这个初始分析提供了所需证明边界的下限。在这个步骤中，由于设计初始化，多个输入流，长输入分组等，我们在附加的证明深度中分层。对于大多数设计，可以通过在输出数据有效端口收集查看覆盖率来获得延迟数。随着输入约束的加入，估计这些值会发生很大变化。如果在初始阶段获得了意外的等待时间，这对我们也是有用的。例如，在复位之外，设计可以执行自动硬件初始化序列。在此期间，设计将不接受任何输入，也不会生成任何输出。设计中观察到的延迟数将突出显示这一点，并且验证工程师可以通过短路初始化过程（如果与测试下的功能无关，通过应用切割点和约束）来开始处理硬件初始化，或者通过提供后硬件初始化设计状态作为初始状态应用到形式工具上。

2.微体系结构分析

这包括识别主要的设计结构。状态机，计数器，FIFO，RAM，链表。这可以通过RTL设计人员的帮助或通过RTL设计的分析来完成。可以编写形式覆盖属性以使每个设计结构处于有效的状态，以获得所需的验证深度的估计值。例如，我们可以找出填充FIFO所需的最小周期，或者遍历状态机所有状态所需的时间。

3.涵盖有意义的conner

此步骤类似于在模拟仿真中对功能覆盖目标列表的分析和创建。这涉及一些有趣的应用场景，以执行RTL的不同角落。我们也需要仔细过滤掉与实际RTL功能无关的角点。这类似于编码用于模拟的功能覆盖点时避免错误。例如，FIFO越来越满，计数器翻转似乎是一个有趣的场景;但是FIFO和计数器如果是完全不相关的两个设计结构，那么并且针对两个结构同时到达其各自的感兴趣状态的验证并没有什么意义。

4.形式覆盖

形式覆盖是一些商业工具提供的较新的功能。当形式验证回归运行完成时，用户可以在实现的证明边界内，查看形式测试平台命中的代码覆盖目标。代码覆盖目标与仿真时查看的目标相同，例如，line、expression或FSM覆盖率等。流程是这样，首先运行端到端检查器，并给定形式验证工具报告的验证边界。然后，在单独的形式覆盖运行中，将最小的证明边界作为输入提供，形式覆盖工具会报告在该边界内达到的代码覆盖目标。未在界限内形式验证未验证到的代码部分，就必须手动分析是为什么没有覆盖到。也有可能的情况是，由于在形式测试台中的有意的或无意的过度约束，使得这其中的一部分覆盖率没有达到。

 5.在形式验证期间发现的bug

通常，单个端到端检查器会发现许多错误。对于每个反例（即真实bug，或者由于形式测试平台问题导致报出的错误），我们跟踪每个深度报告的反例的数量（图6是一个典型的图例）。对于图中的数据，如果形式验证技术在N个周期的深度报告第一反例，并且随后证明在更高深度（例如图6中的N + 6）没有故障，通常这个更高深度是形式验证所需的验证深度。

6. 辅助分析
迄今为止描述的许多步骤都是手动分析，并且可能低估所需的验证界限。虽然这种工作方式也不错，我们很多成功的项目都表明这一方法是有效的，我们还是喜欢额外使用几种方法使验证更全面可靠：
A.通过模拟发现的Bug。通常形式验证与仿真并行执行，或者在更高级别上执行仿真（用于形式验证的DUT包含在用于仿真的DUT中）。如果通过仿真在形式验证DUT中发现错误，我们总是试图在形式测试台中重现这一错误。这个过程表明我们对所需验证深度的分析是不正确的。我们经历了一个情况，当我们忽略了一些微结构条件时，我们对所需验证深度的原始分析需要返工。
B.混合形式搜索。形式工具具有在设计中从深层状态进行搜索的能力。一旦形式验证平台成熟，我们经常设置每晚回归运行，其中一些运行以混合模式运行。如果我们的验证深度分析不正确，混合形式搜索可能会报错，需要重新分析。
二. 抽象模型
我们经常会碰到这样一种情况，design中某一深度的验证对我们很重要，但是直接使用形式验证达到此深度又不太现实，各方面成本太高。这时手动制作一个抽象模型通常可以减少所需的验证深度。
抽象模型用于减少设计的状态空间，这样就大大减少了向更深层次搜索所需的时间。可靠有效的抽象模型不但不会删除任何有效行为，还能为我们提供一些有意义的验证场景。通过向设计添加复位状态或状态转换，可以减少原始设计的状态空间深度，而且某一深度的行为会大大减少，这对快速验证是十分有帮助的。当然也存在假故障（假的bug，来自抽象模型而不是真正的设计bug）的可能性，但是这样的故障都可追踪的，可以用以调试，然后确定它是DUT错误还是由于我们过度抽象造成的。
通常会通过以下方法得到抽象模型
本地化：在设计中添加切点
反抽象：用抽象计数器替换深计数器，例如。直接用0或1代替n位计数器的2N个状态空间
标记：通过简化特定结构来优化由大量数据类型组成的系统
因为抽象模型是与设计紧密相关的，因此首先需要分析被测设计（DUT）以了解形式复杂性的来源，然后制定特定的抽象模型来克服这种复杂性。抽象模型制作的前提是不能错过真正的设计bug，但是粗糙的抽象模型一般都会有假故障，所以制定正确的抽象模型来解决复杂性问题一般是一个不断迭代的过程，最终得到可靠的抽象模型。
三.结束语
在待验证设计越来越复杂的今天，这篇paper旨在向我们展示一种更可靠有效的形式验证流程。核心解决了如何确定一个有效的形式验证深度或边界，这种方法使得形式验证工作更加可量化。原文也给出了两个基于此方法进行验证例子，感兴趣的读者可以查看原文《Sign-off with Bounded Formal Verification Proofs》。