通过形式验证找到更多Bug

经常有这样的事情发生，有些人总可以钓到很多鱼，而其他人却没有这样好的“运气”。之所以这样，很大程度上是因为那些成功的钓鱼者们知道最好的钓鱼点。他们知道鱼儿一般会藏在哪里，就会在哪里放线。

同样，验证的方法也可以引导我们找到合适的“钓鱼点”，大大增加我们捕获bug的数量。

本文提出了一种方法，它利用功能仿真活动，从仿真轨迹中找到有价值的“钓鱼点”，进行形式验证。我们称这种方法为“河钓法”，它并不是从一个初始状态开始形式验证，而是从功能仿真轨迹中挑选出一些可疑的点，然后从这些“钓鱼点”开始形式验证。

河钓法包含三个主要步骤：

●从仿真轨迹中识别并提取出一组合适的“钓鱼点”。

●根据形式验证引擎运行状况筛选并确定这些钓鱼点的优先级。

●在计算服务器上启动并监测多个形式验证的运行。

本文分享了我们最常用的钓鱼点，这在许多设计都可以找到；文中还说明了如何使用形式验证引擎来确定优先级、引导bug寻找过程，从而在形式回归环境中提高验证结果的质量。

我们开始钓鱼吧

在河钓技术中，我们并不是从一个初始状态开始形式验证，而是从功能仿真轨迹中挑选出一些可疑的点，然后从这些点开始进行形式验证。如果功能仿真已经进行了一些与目标有关的值得关注的活动，那么还可以找到其它一些不错的钓鱼点。此外，如果某些目标要求特定的前提条件，则可以利用不同的功能测试，为这些特定目标确定不同的钓鱼点。

实际上，河钓法利用了功能仿真已经执行的任务，来检查那些尽可能接近最终目标的可疑的初始状态，如图1所示。

图1：从一些有趣的钓鱼点启动形式验证。（来源：Mentor）

在以下章节中，我们将详细描述利用河钓法寻找bug的三个主要步骤（如图2所示）:识别钓鱼点、引擎健康筛查，以及并发形式验证运行。

图2：使用河钓法进行形式验证。（来源：Mentor）

寻找最佳钓鱼点

钓鱼专家们都知道，最好的钓鱼地点是河流中那些有着不寻常活动的特殊区域。从仿真轨迹中挑出值得关注的点进行形式验证也与之相似。

图3：确定值得关注的钓鱼点。（来源：Mentor）

这里介绍一个快速全面的两层法，用于挑选那些要关注的钓鱼点。该方法的主要标准包括：

●接口交互：模块间通信和标准协议接口。

●控制和中断：包括FSM、总线控制器、内存控制器、流程图、算法控制等。

●并发事件：包括设计中的仲裁器、调度器、开关、多路复用逻辑等。

●反馈、循环和计数：包括FIFO、定时器、计数器等，用于处理设计中的数据传输、突发和计算。

●用户自定义断言和覆盖属性。次要标准与主要标准的纳入或排除有关。

●纳入标准：收集主要钓鱼点时，应该标记价值高的点，例如满足多个标准的状态、变化频率较低的状态以及出现新活动的状态。

●排除标准：同时，要过滤掉价值不高的钓鱼点，例如重复的状态、导致错误结果的错误状态，以及上电、重置、初始化或配置顺序的状态。

选择最佳钓鱼点

形式验证不同于仿真。仿真运行是可预测、可完成的。但当对大量的断言进行形式验证时，很难预测何时以及是否会完成。因此，了解形式验证引擎的运行状况，并利用它来衡量形式验证取得的进展非常重要。

引擎运行状况可用于衡量通过形式验证取得的进展。而且，形式验证引擎健康是一个矩阵，可用于估计、确定优先级并监测形式验证运行。利用形式验证引擎健康状况，我们可以评估钓鱼点的成果，筛选出低质量的点，并对其余点进行优先排序以进行形式验证。在这些随后的形式验证运行期间，需要持续监控其引擎健康，以便尽早终止那些无效的运行，节省资源来运行新的形式验证。

我们用一组参数来定义形式验证引擎运行状况：

●达成的形式验证目标（proven/fired/covered/uncoverable）（已证明/被终止/被发现/无法发现）。

●探索的顺序深度或分析的影响锥(cone of influence)。

●获取的形式验证知识和引擎设置。

达成的目标和探索的顺序深度是两个完善的指标，已经普遍用于确定形式验证的总体运行进度。

另一方面，如果想了解形式验证在单个属性或目标上的表现，就必须更深入地研究影响锥以及通过这些目标获取的形式验证知识。影响锥提供了关于每个目标探查深度的更多信息，以及扇入逻辑及其对目标依赖性的信息。影响锥突显出扇入逻辑中的“绊脚石”，这时形式验证会被挂起，需要花费大量时间进行分析。这种难解的设计元素是可以被识别的，用户可以决定是否有必要进行干预。有效分析“绊脚石”并解决的方法包括：添加切点、抽象出设计元素，或启用某些特殊引擎。

一直以来，形式验证引擎运行状况被用于监测计算密集型的形式验证的运行。直到最近，我们才意识到它也可以是筛选钓鱼点的好方法。由于要在有限的计算资源（和许可证）上执行大量形式验证，我们发现经常需要不断地终止那些可能徒劳无功的运行。形式验证引擎健康参数可以用于确定计算服务器是否被分配来彻底探测这些钓鱼点。

图4：用引擎健康状况来筛查钓鱼点。（图片来源：Mentor）

放置多条钓鱼线 

有了钓鱼点优先级列表，就可以在服务器集群环境中同时启动大规模形式验证测试了。主服务器将管理和监测所有形式验证过程，它将持续不断地从每个形式验证运行中收集形式验证引擎的健康参数。图5捕获了一个形式验证运行开始时的目标分布，用户可以由此知道已经取得的进展。最初，33个目标中的大多数是不确定的 ，即inconclusive（I）。在多核并行的情况下，形式验证逐渐验证目标，并将它们划分为以下几个类别之一：firing (F)、vacuous (V)、uncoverable (U)、covered (C)和proof (P)。

图5：形式验证目标被证明或满足的快照。 （图片来源：Mentor）

一个全面的形式验证工具都具有一组形式化引擎，用以处理不同结构的设计。随着形式验证的运行，可以检查引擎的状态，以了解哪些引擎可以得出结果，而哪些引擎可能不会有收获。如果某个引擎对当前的任何结果都无贡献，可以将该引擎替换掉以节省资源，并将其它引擎集中在当前任务上。图6是一个分布式形式验证运行期间的引擎快照。

图6：形式验证引擎知识库快照。（图片来源：Mentor）

 “Proven/Unsatisfiable”列显示了哪些引擎可解决安全性、寿命、空白和覆盖类型检查。 “Fired/Satisfied”列显示了哪些引擎生成了反例。引擎7在查找大量证据和终止(firing)方面贡献很大。引擎0（管家引擎）和引擎10也找到了一些证据。另外，引擎12和17（针对某些难题设计）虽然也致力于解决问题，但并没有什么产出。“Inconclusive Targets”列（好、中、差）则显示了工作中(WIP)目标的单个引擎健康状况。引擎12正在研究75个健康状况良好的目标，也就是说，它进展顺利，只有三个目标健康状况中等和不良。同样，引擎10在51个属性上运行良好，但在其它很多目标上运行无效。

钓鱼收获如何？

在以下案例中，我们捕获了两种代表性的bug情况。而且只有在我们从仿真轨迹深处的钓鱼点开始形式验证之后，才成功捕获。形式验证引擎健康筛查也被用来清除许多不成功的验证运行，这在开始或验证过程中都可能发生。

图7：比率同步数据传输接口。（图片来源：Mentor）

案例一：为节省能耗，如今的设计中都应用了很多比率同步时钟，它们尽可能慢地运行每个组件。因此，比率同步接口很常见。在数据有效条件确定时，这些接口中的快速时钟域被设计为在慢时钟周期结束时对数据进行采样。但是，在某些特殊情形下（设计团队最初不知道），即使未声明有效条件，数据也会被采样。结果，损坏的数据被注册并在系统内传递。根据两个接口、计数器和控制逻辑上的活动可以确定钓鱼点。在初始化设计之后，以及两个接口之间的数据经过数百个周期的正确传输之后，挑选出几个钓鱼点。形式验证揭示出两个接口之间不完整的握手信息，这种不完整导致数据采样无效。

案例二：在此数据传输控制器中，设置了动态传输通道以处理具有不同优先级的数据包。 在这种情况下，当多个通道同时完成传输时，一组地址指针将被解除分配两次，而另一组地址指针却没有被解除分配，从而导致内存泄漏和数据损坏。根据并发事件、计数器和复杂控制逻辑的活动可以确定钓鱼点。在这种类型的设计中，形式验证很难设置这些数据传输。但是，它们很容易在仿真回归中获得。通过利用仿真运行深处的多个钓鱼点，并基于引擎健康对它们进行优先排序，形式验证可以暴露通道去分配逻辑中的弱点，并同步两个通道以同时完成传输。

图8：数据传输控制器。（图片来源：Mentor）

河钓技术

河钓技术利用了功能仿真活动，从仿真轨迹中找到可疑的捕鱼点开始形式验证。识别一组合适钓鱼点的标准有很多，包括接口交互、控制和中断、并发事件、反馈循环和计数、用户自定义断言和覆盖属性等。然后，根据形式验证引擎健康状况对这些钓鱼点进行筛选和优先级排序，可以被定义为：已证明或已摒弃的验证目标、已探查顺序深度，以及所获取形式验证知识库。之后，当集中式数据库将所有结果汇总在一起时，使用一组钓鱼点来初始化多个形式验证运行。根据得出的结果和发现的复杂bug，我们可以看到，在形式验证回归环境中，河钓技术确实有助于提高验证结果的质量。

（参考原文：Catch More Bugs with Formal Verification）

责编：Amy Guan

本文为《电子工程专辑》2020年5月刊杂志文章，版权所有，禁止转载。点击申请免费杂志订阅