形式验证成为SoC模块验证的主流

使用形式验证技术作为片上系统 （SoC） 设计的主流技术，终于成为消除验证差距的公认方法。最近的一项调查表明，26% 的芯片设计项目现在使用基于断言的正式验证 （ABV）。然而，这种经典模拟的替代方法的承诺需要很多年才能开花结果，而且仍然只有高级验证环境才能包含它。为什么会这样？到目前为止，我们可以从它的使用中学到什么，以便将其提供给整个 SoC 工程社区？

SoC 块验证碰壁

自问世以来，SoC 设备一直是开发团队的验证噩梦。虽然现在验证完整的 SoC 最好留给仿真和快速原型设计系统来完成，但即使是这些设备上的较大块也已经超出了纯仿真环境。

仿真、更快的模拟器、关键测试的验证知识产权 （VIP） 以及通用验证方法 （UVM） 的出现都有助于缓解这种情况。尽管如此，验证要求仍超过了基于模拟的环境中的可用处理时间。

形式验证通过使用针对特定需求的自动化“应用程序”有助于改进块验证，否则需要大量的模拟工作。检查标准通信协议的正确操作、确保关键连接和寄存器操作、分析域重置时的正确启动序列以及许多其他任务现在都由这些解决方案处理。

然而，我们才刚刚开始挖掘形式验证的真正威力。它的许多使用问题已被消除，使我们处于可能是全新验证时代的最前沿，因为该技术已部署用于核心验证。

形式验证：如果这么好，今天在哪里？

首先，快速回顾一下形式验证技术，为什么它有可能创造这种根本性转变，以及今天是什么阻止了它。

硬件仿真的工作原理是通过一系列有意义的状态循环一个硬件描述语言 （HDL） 代码块来演示其操作。此状态序列由输入激励（设备输入上的一组事件的 HDL 描述）驱动，旨在探索正确的状态以识别操作问题。

这种方法引出了一个问题：如果我们知道代码块可以进入的所有状态以及状态间转换，那么我们不能简单地询问有关代码操作的问题以确保其正确吗？这将避免必须编写许多行刺激来尝试使代码块进入正确的信息承载状态。这是形式验证工具使用的方法。

这种基本方法可以转变为许多有用的应用程序。例如，如果可以根据设计代码的一个方面和要检查的验证场景自动创建要问的问题，则可以创建用于验证目的的自动化应用程序。这将不需要用户编写问题。如果正式工具可以用最少的输入演示特定的状态序列（例如状态机操作），那么设计工程师就可以理解他或她的代码如何执行，从而揭示可能的错误。

当工程师自己提出问题时，形式验证的真正威力才得以发挥。这需要使用断言编写问题或属性，并在称为基于断言的验证或 ABV 的过程中应用于设计。

当然，这种高级描述掩盖了 ABV 的问题，包括存储这么多信息的工具的容量和性能要求已经通过最新技术得到解决。

两个问题仍然是 ABV 广泛使用的障碍：

断言的创作，通常使用 SystemVerilog 标准语法，可能很复杂且难以可视化

对验证进度或覆盖率的理解很难与其他验证方法的理解和对比

尽管在这两个方面都取得了进步，但还需要更多的努力来降低学习曲线，从而使 ABV 得以普遍扩散。

ABV 应用程序

在验证过程中应用 ABV 有两种常用方法。首先是检查特定的极端案例类型的问题，这些问题通常需要花费大量精力来构建模拟测试平台来分析问题。第二个是对块进行更一般的检查，无论是结合模拟还是独立检查。

形式验证的第一个使用模型很有价值，可以在验证计划中减少合理的百分比。第二个模型有可能改变特征验证过程，节省大量时间和资源支出，同时增加发现设计中每个错误的整体潜力。已经有一些行业部门在第二种模式中广泛使用 ABV。其中包括汽车和航空电子产品，其中高质量和可靠性是一个因素。

在组合仿真-形式验证流程中，如图 1 所示，通常使用仿真进行一般操作分析并“感受”设计的行为和性能。此外，还有一些功能更适合模拟，例如数学数据处理或信号处理。然而，形式验证非常适合控制或数据传输种类的功能，如有限状态机、数据通信和协议检查。此外，确保某些类型的验证场景，例如安全检查（例如，某项活动是否会发生），也是该技术的最佳选择。这些代码和场景示例通常需要很高比例的验证资源。

断言创作改进

与 UVM 推动模拟测试台创建的分层方法相同，新技术正在出现，将抽象引入断言创作。这些抽象通过掩盖断言细节来降低复杂性，同时允许工程师考虑验证任务而不是断言的个别特征。

例如，OneSpin 解决方案的 Operational Assertions 是一个 SystemVerilog 库，它允许正式测试以类似事务时序图的方式表示，与验证工程师广泛认可的高级 UVM 序列不同。Breker Verification Systems 的基于图形的测试序列，现在由 Accellera Portable Stimulus 标准委员会考虑，是另一种抽象形式，也可以应用于断言创作。

这些技术在简化形式测试应用的同时，具有提供可识别且更自然的输入方案的优势，允许工程师通过消除一些形式验证之谜来与正在进行的验证过程相关联。

常见的覆盖模型

简化断言只是难题的一部分。该过程的另一端是整理来自各种来源的覆盖率信息，以了解总体验证进度，无论使用何种工具。模拟过程仍然主要集中在一种或另一种代码覆盖上，并包含一些功能覆盖。形式验证覆盖侧重于断言（所谓的“断言覆盖”），无论它们是否被执行，它们是通过还是失败，或者确实它们通过一个警告（例如，有界证明，例如“代码在一定数量的时钟周期内通过”）。该信息可以反馈给验证计划系统以提供一些有用的数据。

然而，测量正式的覆盖率，确定由特定断言测试的实际代码，是领先的形式验证供应商感兴趣的领域。已经提出了在精度和所需执行资源方面都不同的方案。关键是能够将这些正式模型与模拟模型进行比较，以提供综合的、有意义的覆盖率评估。Accellera 统一覆盖互操作性标准 （UCIS） 委员会专注于这一目标，并提出了可以将两者进行比较的方法。在这方面需要做更多的工作，但很明显，一些形式验证供应商拥有允许计算合理的进度度量的解决方案。

模拟风格调试

以对以仿真为中心的工程师有意义的方式调试形式验证代码，在很大程度上已被许多形式验证供应商解决。大多数工具可以在断言失败的情况下输出“见证”。也就是说，导致断言失败的仿真波形形式的一系列事件。事实上，包括 OneSpin 在内的一些供应商可以输出模拟测试，允许在模拟器中重现故障以供进一步研究。

破解主流ABV代码

很明显，ABV 的使用开始成为主流。ARM 和 Oracle 都宣布了 ABV 在其环境中的全部功能，并指出它现在在他们的项目中被大量使用。

解决 Assertion Authoring、Collated Coverage 和 Simulation-centric Debug 这三条腿的问题，并将其与对形式验证擅长的设计领域和场景的清晰理解相结合，将推动这种方法成为 SoC 验证的主流。一旦发生这种情况，将对未来的设计质量和开发进度产生巨大影响。

审核编辑：郭婷