芯技术 | IC设计：基于形式化方法的验证找bug

众所周知，硬件是芯片世界的新货币。半导体行业不再是传统半导体巨头的天下；越来越多的软件公司现在拥有自己专门的硬件开发团队。随着开源架构的出现，用开源框架和工具开发芯片渐渐成为主流。

然而，虽然芯片设计变得更容易了，但芯片验证却没有。

2020年威尔逊研究小组功能验证研究(Wilson Research Group Functional Verification) 指出，83%的FPGA和68%的ASIC设计在第一次流片尝试中失败。同样值得注意的是，68%的ASIC项目实际执行低于预期。

调查报告指出，对于处理器的开发，验证工程师和设计工程师的比例是5:1。想象一下，要雇用比设计多五倍的验证资源，还要面对芯片重新流片的情况。

应用软件更新来修补硬件缺陷的现状并不总是一个可行的选择，特别是当验证成本估计约占整个项目成本的70%。

当1995年英特尔奔腾FDIV的bug出现时，计算机主要是作为桌面PC或服务器使用。如今，从汽车和物联网设备到5G移动电话，计算机的使用无处不在，在国防和航空航天领域的应用也在不断增加。

功能验证并不是唯一的挑战。对于ISO 26262、DO-254和DO-333等不同的标准，责任与建立可靠性同样重要。作为Meltdown和Spectre漏洞的后续，安全防护问题也随着功能安全问题而日益突出。

随着硬件开发和上市时间的需求和竞争，对质量和可靠性的要求也同步增加。

软件动态仿真一直是传统的芯片验证主力，并且仍然是数字和模拟电路设计验证中的主导技术。在系统级验证中常常用到硬件加速仿真，尽管它的前期成本很高，但任何重视硅片质量的公司都在使用。硬件加速仿真提供了更高的速度，是一种更快的仿真形式。

动态仿真和硬件加速仿真都利用了测试案例，并使用输入序列或程序作为测试底层硬件的主要形式。如果在这些环境中设计的预期行为和实际行为不匹配，就会被标记为设计或测试bug。测试案例只能显示bug的存在，而不能证明其不存在。

在20世纪70年代引用Dijkstra的算法作为形式化方法的一个案例，这在2022年仍然是如此。验证的强度取决于其最薄弱的环节，而动态仿真和硬件加速仿真最薄弱的环节是用于验证特定场景的特定测试案例的输入序列。

当然，现代仿真使用功能覆盖率来保证已经做了足够的测试，但不能保证进行彻底的验证。换句话说，测试平台清除了所有采用动态仿真和硬件加速仿真方式发现的bug。

形式化方法使用一种以证明为中心的技术，即形式化工具构建设计和测试平台的数学模型，以证明，表示为断言或覆盖目标的给定需求被充分证明。

形式化方法能够证明这一点的原因是，从根本上说，形式化使用了来源于人工智能的搜索技术，并将逻辑推理和决策用于设计的符号化显示上。

基于形式化方法的验证在硬件的符号模型上工作。它自动抽象出设计空间的指数级复杂性以建立一个断言或覆盖属性的证明。如果不能建立证明，工具会显示一个反例波形，就像在仿真中一样，它可以用来修复设计bug。由于形式化工具以智能方式进行详尽的搜索，所以通常可以更快找到容易忽略的bug，而且在许多情况下，比通过仿真或模拟测试平台更容易发现更多bug。

对于许多验证问题，形式化方法是无可替代的。例子包括证明：

没有死锁：定点和浮点等算术量大的设计的代码覆盖正确性不可达。

微处理器的鲁棒性验证，特别是失序的、超标量的：具有深层计数器、FIFO和存储器组件的并发设计的正确性。

所以，形式化方法已经成为经验丰富的设计验证组处理许多这类问题的唯一选择。

在一个典型的项目中，仿真是用于验证的主要技术。众所周知，一个相当复杂的通用验证方法（UVM）测试平台的开发时间是几周或几个月，而这仅仅是为了开始测试少数几个有趣的、有针对性的测试案例。

另一方面，对于大多数设计项目来说，建立形式验证只需要几天时间。而且，尽管形式化测试平台并不完全完整，但由于以证明为中心的状态空间搜索的性质，在形式化工具中测试时的断言提供了更广泛的调查范围，并且能够更快、更全面地识别bug。

结合形式化和仿真，设计验证小组能够在设计的第一周就开始使用形式化来发现bug。当仿真和测试平台准备好的时候，形式化就已经清除了显而易见的bug和容易忽略的bug，而这些bug可能会对仿真造成挑战。

形式化方法可能存在可扩展性问题，这时可以将一些艰难的工作转移到仿真测试平台上。上图显示了形式化方法在项目中的部署是如何从前五个开始到最后五个中发现bug的。

当与仿真相结合时，这两种技术提供了一个非常强大的框架，用于寻找bug和建立不存在bug的数学证明，这对于功能安全和保障是非常需要的。通过结合形式化和仿真，设计验证小组可以继续在形式化中运行断言和覆盖属性，并在仿真环境中重新使用它们。有必要在仿真环境中回归形式化的属性，以验证它们的接口，因此可以排除形式化中的任何不正确的假设。

当仿真测试平台在诸如X-检查、异步检查、寄存器检查、连接性、死锁和不可达的代码覆盖率分析等问题上的能力开始耗尽时，形式化应用通常在项目生命周期的最后阶段才会启动。在这个阶段，设计验证小组通过利用自动化形式化应用的力量来解决他们最后的五个bug。

设计验证小组如何在大型项目设计中通过形式化验证发现1000万甚至1亿多次的失败？用形式化验证结束这些芯片设计功能区块指令有哪些诀窍？这个答案简单来说就是——需要一个很好的方法论。

为了使形式验证属性检查能够更快地找到bug并且不受工具容量问题的影响，必须掌握形式方法的一些基本面。通常，如果提出正确的问题，该工具可以更快地促进事情的发展，而不会出现著名的“状态空间爆炸”问题。

一种抽象驱动的方法学提供了一种解决设计复杂性问题的好方式。敏捷流程可能是在项目上部署形式验证的理想流程，可以最大限度地发挥其真正潜力。

避免

检测

删除

证明

流片

以敏捷的方式进行形式化的美妙之处在于，当工程师不断通过更改设计迭代产品时，他们会按照流程在每次迭代中挑出bug。例如，工程师不必等到代码完成便可查找出设计中的死锁。

这六个维度强化了核查工作的定性和定量性。一切都从需求开始，这些需求为制定正式的断言和覆盖目标列表铺平了道路。

第一个维度是定性的维度，其驱动力是：验证组将要验证什么，签核的覆盖目标是什么？它自需求而生，并被形式化为目标断言和覆盖属性在工具中执行。

第二个维度确定在形式工具中证明了多少断言和覆盖点（通过或失败）。此数量是断言覆盖率，它提供了验证运行实现多少的定量视图。在这个阶段，验证组不知道检查器（断言和覆盖）是否做了任何有用的事情或执行了所有的设计代码。

第三个维度提供了对检查器完整性的见解。这是一个定性维度，通过对测试平台进行彻底审查以及插入一些新bug来测试检查器是否正在检测出这些人为引入的bug来解决检查器的质量问题。

通常，通过好的设计和没有原生bug的情况下，验证工具可以构建证明，于是工程师便想知道为什么我们没有发现任何bug。为了解决这个问题，手动插入的bug提供了一种快速确定检查器是否合理的方法。此过程还有助于发现设计中的任何过度约束，这些约束可能会阻止在形式验证测试平台中注入合法有效的激励。这是称为过度约束分析的第四个维度，这是一种急需的定性评估，以发现潜在的关键测试平台bug。它为发现以前由于过度约束而未发现的新的设计bug铺平了道路。

第五个维度是一种工具驱动的自动化方法，用于发现在属性验证期间执行和达到哪些设计代码。这是一项按钮工具功能，可用于发现没有检查器或约束阻止代码可访问性的盲点。在此阶段发现标准代码覆盖率问题。

第六个维度称为场景覆盖，它提供了一个类似功能覆盖的定量视图，用于验证在处理功能执行的已知场景方面有多好。验证团队填充所需方案的电子表格，该工具会自动将它们合成为这些特定方案的断言和覆盖目标，并在形式工具中对其进行测试。它提供了面向视觉和指标的覆盖属性视图，并显示了这些特定场景的证明，因为知道这些场景经过了详尽的测试，因此毫无疑问地验证了这些场景。

来源：酷芯微电子

作者：ASHISH DARBARI

翻译：酷芯PR团队

校对：酷芯芯片验证团队

END