形式验证最佳实践之五：收尾和总结

这是形式验证最佳实践系列的最后一集。作为最后一步，让我们来讨论一下正式验证和总结。在使用形式验证验证高速缓存控制器之后，我们的成果超出了预期。我们重现并验证了已知死锁的设计修复。我们还验证了数据完整性和协议合规性。但是，我们在做这些工作时并没有考虑高速缓存微体系结构，因此我们没有任何嵌入式断言。

现在的问题是：我们完成了吗？这样的验证是否足够？通过一些小技巧，我们能够获得了证明，但我们是否观察到了所有可能的漏洞？我们通常可以通过形式覆盖来回答这些问题。

正式覆盖分类法

在收集覆盖率之前，我们首先需要定义我们想要观察的内容。与模拟中的代码覆盖类似，正式覆盖可以观察分支、语句、条件和表达式。它还可以观察功能覆盖所定义的覆盖点。所有这些都被称为 "覆盖项"（CI）。在实践中，我们发现如果存在分支、语句和覆盖点，选择它们就足够有用了。

实际上，正式覆盖有不同的类型。让我们来看看它们。

可达性覆盖

这需要进行正式分析，以确定每个 CI 是否可以覆盖。这与在模拟中测量代码覆盖率非常相似。它完全独立于断言。

静态覆盖率

静态覆盖也称为 "影响范围"（COI）覆盖。它不需要运行任何形式分析。如果每个 CI 至少出现在一个断言的 COI 中，则标记为已覆盖。

可观察性覆盖

这需要对断言进行形式分析。在分析过程中，证明引擎会报告对完成证明至关重要的 CI。

此时我们需要注意的是，有界证明也有助于提高覆盖率。突变覆盖率是一个非常相似的指标，但使用的是不同的技术。它不能很好地扩展形式覆盖率。

有界覆盖率

如果某些断言未被穷举证明，则将证明约束与 COI 中 CI 的约束（通过可达性覆盖率获得）进行比较。

现在，让我们更详细地了解前三种覆盖类型。

谁擅长什么？

下表显示了每种覆盖都能检测到哪些问题，括号中标出了主要问题。

在时间/CPU 预算允许的情况下，可达性覆盖率很好地说明了形式化工具分析设计的能力。如果覆盖率不足，则意味着需要添加新的抽象概念。这种覆盖率还能告诉你哪些代码片段没有被覆盖，因为它们是死的（设计问题），或者因为约束条件阻止了覆盖（形式化测试平台问题）。

静态覆盖可以让你快速了解设计中哪些部分肯定没有被任何断言检查。如果必须对这些部分进行形式验证，则需要添加新的断言。由于设计的性质，这种覆盖率通常很高，而且很容易实现。但这并不能让您满意！

可观察性覆盖率，也称为 "证明覆盖率"，可能是最重要的覆盖率。它总是静态覆盖的一个子集。事实上，某些逻辑可能在特定断言的 COI 中，但实际上并不在该断言的可观察性覆盖范围内。这意味着，只看静态覆盖而不看可观测性覆盖是一种过度乐观主义，也是一个巨大的错误！

例如，下面蓝色气泡中的逻辑非常庞大和复杂。断言写成

o_always_high: assert property(o)；

这个断言很容易证明。可以静态覆盖整个逻辑气泡。但可观察性覆盖范围实际上只包括所示的逻辑：3 个触发器和 2 个门。其余逻辑与证明该属性无关。

我们在高速缓存控制器上覆盖了哪些内容？

让我们分三步来考虑高速缓存的验证，由于死锁验证非常特殊，我们将其分开。首先，我们验证了顶层接口是否符合 AHB 规范。然后，我们验证了一个关键断言，检查是否发生多重命中。最后，我们验证了数据完整性。

现在，让我们看看覆盖率如何。

可达性覆盖率

我们首先测量了可达性覆盖率，因为它与断言无关。在这个相对较小的设计中，覆盖率非常高。漏洞只是一些死代码。如果我们移除抽象，尤其是无效计数器上的抽象，覆盖率就会下降，从而证实了这些抽象的有用性。

使用 AHB 协议检查器的覆盖率

在添加协议检查器验证 AHB 合规性后，静态覆盖率已经非常高了。事实上，一个断言，例如在等待确认时检查数据总线的稳定性，其 COI 中几乎包含了整个设计。即使是与维护操作相关的逻辑（我们知道任何断言都无法直接验证），也被涵盖在内。这一指标中唯一的漏洞出现在事件计数器上。

但从可观察性覆盖率来看，其覆盖率相当低。事实上，协议断言非常 "本地化"，只需要靠近顶层接口的逻辑。例如，处理查找、命中/未命中计算、触发补线和驱逐的逻辑在这里就没有涉及。这并不奇怪。

多个命中断言的覆盖率

在添加了检查是否存在多重命中的断言后，我们再次测量了覆盖率。静态覆盖率保持不变。几乎已经达到最大值。

然而，可观察性覆盖率显著增加，尤其是在控制主导的代码块上。这是因为仅断言一项就需要验证大量逻辑。这些逻辑在上一步中没有涉及。但仍存在一些漏洞：事件计数器以及处理数据传输到设计中的逻辑（虽然规模不大，但却是必不可少的）仍未涵盖。这些逻辑包括一些多路复用器和缓冲器，用于保存数据并在不同位置之间传播。

数据完整性断言覆盖

我们添加了端到端断言，以验证数据完整性。同样，静态覆盖率保持不变。可观察性覆盖率略有增加。通过观察差异，我们可以发现数据传输的逻辑已被覆盖。

唯一的漏洞还是关于事件计数器。这很容易解释：根本没有关于这些计数器的断言。而且，除了在外部提供其值外，设计内部并没有使用它们。使用断言和形式来验证这一点可能不是一个好主意。这需要对命中、未命中、驱逐等条件进行繁琐的建模。这最好使用仿真测试平台来完成。

您可以构建一个 "覆盖率热图"，并在添加新属性、抽象或约束时对其进行更新。对于我们的高速缓存，在我们考虑的三个步骤中，代表可观察性覆盖范围的热图如下所示。绿色区域已覆盖，红色区域未覆盖。

截止到目前，验证任务正式完成了吗？对于这次缓存验证来说，可以肯定地说 "是的"。覆盖率指标显示，我们打算验证的内容确实已经验证。剩下的部分则更适合基于仿真的验证。

为形式化定义目标，并用不同的覆盖率指标来衡量它们，这是件好事。附加值其实不在于数字，而在于检测到的漏洞。你必须仔细观察这些漏洞，并了解它们是否在预料之中。如果不是，就改进你的正式测试平台，添加新的断言等。如果它们是预料之中的，你就必须采用一种或多种其他验证技术来解决它们。

设定覆盖率目标（百分比数字）似乎不是一个好主意。可以肯定的是，最终会留下一些漏洞，这没有问题，因为其他验证方法已经覆盖了这些漏洞。但你不知道这些漏洞的相对大小。

良好的实践

在最后一集中，我们探讨了如何确保在形式化方面做得足够好。以下是一些收获供大家参考。

总结

至此希望大家喜欢Codasip所分享的形式验证最佳实践系列。还有一些其他的形式化技术并没有在这个系列中提到，但它们也非常有用。

例如，X-传播验证可以告诉您是否存在仅在门级，甚至仅在硅片上可见的漏洞风险。这些漏洞尤其难以通过仿真发现。

顺序等价检查是一种多用途工具。它可用于验证时钟门、ECO、设计优化等。在我们的高速缓存中，等价检查被用来确保我们在完整高速缓存配置（IDCache）上所做的所有工作在纯数据配置（DCache）上都是有效的。为此，我们将 IDCache 与 DCache 进行了比较，条件是任何请求都不得以指令部分为目标。对于纯指令配置也是如此。

安全特性也可以通过形式来验证。例如，对于缓存来说，这意味着作为安全请求写入的数据永远不会作为非安全请求的一部分从缓存中流出。侧信道攻击的漏洞也可以用形式来验证。

以上这些额外的知识点为Codasip的验证系列第二季提供了大量素材，期待有机会再跟大家分享和探讨。