众所周知，硬件是芯片世界的新货币。半导体行业不再是传统半导体巨头的天下；越来越多的软件公司现在拥有自己专门的硬件开发团队。随着开源架构的出现，用开源框架和工具开发芯片渐渐成为主流。
然而，虽然芯片设计变得更容易了，但芯片验证却没有。
2020年威尔逊研究小组功能验证研究(Wilson Research Group Functional Verification) 指出，83%的FPGA和68%的ASIC设计在第一次流片尝试中失败。同样值得注意的是，68%的ASIC项目实际执行低于预期。
调查报告指出，对于处理器的开发，验证工程师和设计工程师的比例是5:1。想象一下，要雇用比设计多五倍的验证资源，还要面对芯片重新流片的情况。
图1 从成本上升到项目进度延迟，
再到人员的重新分配，
半导体验证面临的挑战数不胜数。
来源：2020年威尔逊研究集团和Axiomise
应用软件更新来修补硬件缺陷的现状并不总是一个可行的选择，特别是当验证成本估计约占整个项目成本的70%。
挑战：它不再是功能验证
当1995年英特尔奔腾FDIV的bug出现时，计算机主要是作为桌面PC或服务器使用。如今，从汽车和物联网设备到5G移动电话，计算机的使用无处不在，在国防和航空航天领域的应用也在不断增加。
功能验证并不是唯一的挑战。对于ISO 26262、DO-254和DO-333等不同的标准，责任与建立可靠性同样重要。作为Meltdown和Spectre漏洞的后续，安全防护问题也随着功能安全问题而日益突出。
随着硬件开发和上市时间的需求和竞争，对质量和可靠性的要求也同步增加。
软件动态仿真一直是传统的芯片验证主力，并且仍然是数字和模拟电路设计验证中的主导技术。在系统级验证中常常用到硬件加速仿真，尽管它的前期成本很高，但任何重视硅片质量的公司都在使用。硬件加速仿真提供了更高的速度，是一种更快的仿真形式。
动态仿真和硬件加速仿真都利用了测试案例，并使用输入序列或程序作为测试底层硬件的主要形式。如果在这些环境中设计的预期行为和实际行为不匹配，就会被标记为设计或测试bug。测试案例只能显示bug的存在，而不能证明其不存在。
在20世纪70年代引用Dijkstra的算法作为形式化方法的一个案例，这在2022年仍然是如此。验证的强度取决于其最薄弱的环节，而动态仿真和硬件加速仿真最薄弱的环节是用于验证特定场景的特定测试案例的输入序列。
当然，现代仿真使用功能覆盖率来保证已经做了足够的测试，但不能保证进行彻底的验证。换句话说，测试平台清除了所有采用动态仿真和硬件加速仿真方式发现的bug。
形式化方法：一种基于证明的方法
来确定bug是否存在
形式化方法使用一种以证明为中心的技术，即形式化工具构建设计和测试平台的数学模型，以证明，表示为断言或覆盖目标的给定需求被充分证明。
形式化方法能够证明这一点的原因是，从根本上说，形式化使用了来源于人工智能的搜索技术，并将逻辑推理和决策用于设计的符号化显示上。
基于形式化方法的验证在硬件的符号模型上工作。它自动抽象出设计空间的指数级复杂性以建立一个断言或覆盖属性的证明。如果不能建立证明，工具会显示一个反例波形，就像在仿真中一样，它可以用来修复设计bug。由于形式化工具以智能方式进行详尽的搜索，所以通常可以更快找到容易忽略的bug，而且在许多情况下，比通过仿真或模拟测试平台更容易发现更多bug。
对于许多验证问题，形式化方法是无可替代的。例子包括证明：
没有死锁：定点和浮点等算术量大的设计的代码覆盖正确性不可达。
微处理器的鲁棒性验证，特别是失序的、超标量的：具有深层计数器、FIFO和存储器组件的并发设计的正确性。
所以，形式化方法已经成为经验丰富的设计验证组处理许多这类问题的唯一选择。
图2 形式化方法的使用仍然局限于穷举法，
无论是简单的问题还是项目周期的结束。
资料来源：Axiomise
在大多数组织中，形式化方法的使用仍然限于解决简单的问题，如项目开发早期的lint，或在项目后期建立片上系统（SoC）的连接性检查。确实，使用电子设计自动化（EDA）供应商的lint应用程序和连接性检查应用程序来发现bug，但大多数公司还是使用仿真来进行大部分的功能验证。
形式化方法没有得到广泛应用。唯一的例外是，在某些情况下，少数形式化专家会拿着一两个设计块用形式化方法验证，这使得该验证方法在方法采用、方法理论或方法重用方面没有一致性。在整个项目周期中，形式化方法在容易忽略的错bug和建立没有bug的证明方面的真正潜力仍有待开发。
形式化方法的真正潜力是无限的
在一个典型的项目中，仿真是用于验证的主要技术。众所周知，一个相当复杂的通用验证方法（UVM）测试平台的开发时间是几周或几个月，而这仅仅是为了开始测试少数几个有趣的、有针对性的测试案例。
另一方面，对于大多数设计项目来说，建立形式验证只需要几天时间。而且，尽管形式化测试平台并不完全完整，但由于以证明为中心的状态空间搜索的性质，在形式化工具中测试时的断言提供了更广泛的调查范围，并且能够更快、更全面地识别bug。
结合形式化和仿真，设计验证小组能够在设计的第一周就开始使用形式化来发现bug。当仿真和测试平台准备好的时候，形式化就已经清除了显而易见的bug和容易忽略的bug，而这些bug可能会对仿真造成挑战。
图3 形式化验证可以在广泛的验证范围内部署。
资料来源：Axiomise
形式化方法可能存在可扩展性问题，这时可以将一些艰难的工作转移到仿真测试平台上。上图显示了形式化方法在项目中的部署是如何从前五个开始到最后五个中发现bug的。
当与仿真相结合时，这两种技术提供了一个非常强大的框架，用于寻找bug和建立不存在bug的数学证明，这对于功能安全和保障是非常需要的。通过结合形式化和仿真，设计验证小组可以继续在形式化中运行断言和覆盖属性，并在仿真环境中重新使用它们。有必要在仿真环境中回归形式化的属性，以验证它们的接口，因此可以排除形式化中的任何不正确的假设。
当仿真测试平台在诸如X-检查、异步检查、寄存器检查、连接性、死锁和不可达的代码覆盖率分析等问题上的能力开始耗尽时，形式化应用通常在项目生命周期的最后阶段才会启动。在这个阶段，设计验证小组通过利用自动化形式化应用的力量来解决他们最后的五个bug。
方法论：使形式高效、
可预测和可扩展
设计验证小组如何在大型项目设计中通过形式化验证发现1000万甚至1亿多次的失败？用形式化验证结束这些芯片设计功能区块指令有哪些诀窍？这个答案简单来说就是——需要一个很好的方法论。
为了使形式验证属性检查能够更快地找到bug并且不受工具容量问题的影响，必须掌握形式方法的一些基本面。通常，如果提出正确的问题，该工具可以更快地促进事情的发展，而不会出现著名的“状态空间爆炸”问题。
一种抽象驱动的方法学提供了一种解决设计复杂性问题的好方式。敏捷流程可能是在项目上部署形式验证的理想流程，可以最大限度地发挥其真正潜力。
图4 通过实施敏捷的形式验证流程，
可以降低设计复杂性
1
避免
在设计开发的第一个小时内使用形式验证工具。一旦编写了第一行代码，验证工程师就应该运行一个形式化工具来编译和综合。他们需要检查悬空的连线、不匹配的信号类型、未驱动的连线、复位/非复位bug、死代码和冗余代码等显而易见的bug，并获得代码覆盖率报告。是的，大多数形式验证工具都可以在运行工具并识别第一个缺陷的几秒钟内提供此信息。放弃形式验证工具而在模块中构建死代码并让仿真测试平台在几个月后找到它并浪费时间来解决代码覆盖率问题，这是没有意义的。
2
检测
以敏捷的方式使用形式验证工具。通过遵循第一步，设计更改的每次迭代都将找出容易解决的bug。但是，工程师可以更进一步，引入接口约束，开始查找与 X 态传播、死锁、FSM 可访问性和活锁相关的问题。大多数分析在大多数工具中也是自动化的（尽管不是全部），工程师可以在几分钟内开始捕获死锁和X态问题。
3
删除
通过使用形式工具的自动化功能以敏捷的方式部署形式，工程师可以构建没有结构设计缺陷（并且没有代码覆盖问题）的设计单元。现在可以将设计移交给验证组进行功能验证，验证组现在可以部署基于断言的验证（ABV），也称为属性验证，以清除bug（删除）。
4
证明
在许多情况下，构建不存在bug的证明在形式工具是很正常的。当形式工具没有bug时，它会构建证据，证明设计将始终针对形式化为断言和覆盖属性的指定要求正确工作。但是，在许多情况下，形式工具无法在合理的时间内自动构建证明，并且工具容量不足。通过遵循结构化的流程和方法，使工程师让任务具备可预测性，也让过程具备确定性。通过部署以证据为中心的技术来实现的，这些技术由拥有硬件设计领域相关专业知识的人提供，并且允许在搜索空间的更深边界进行详尽的证明以及搜索bug。
5
流片
当单个设计模块经过形式验证后，它们将被集成在更大的SoC中，成为一颗完整芯片的一部分。在这里，形式工具可以且应该用于使用协议检查器验证不同设计单元之间的功能接口，识别跨时钟域和复位问题，以及验证寄存器和检查X态。当寄存器传输级（RTL）代码被综合成门级网表时，RTL到门级等效性检查也可以发现任何问题。
以敏捷的方式进行形式化的美妙之处在于，当工程师不断通过更改设计迭代产品时，他们会按照流程在每次迭代中挑出bug。例如，工程师不必等到代码完成便可查找出设计中的死锁。
通过形式验证实现的覆盖率
和sign-off（签核）
图5 六个维度构成了一个完整的
形式验证覆盖流程
这六个维度强化了核查工作的定性和定量性。一切都从需求开始，这些需求为制定正式的断言和覆盖目标列表铺平了道路。
第一个维度是定性的维度，其驱动力是：验证组将要验证什么，签核的覆盖目标是什么？它自需求而生，并被形式化为目标断言和覆盖属性在工具中执行。
第二个维度确定在形式工具中证明了多少断言和覆盖点（通过或失败）。此数量是断言覆盖率，它提供了验证运行实现多少的定量视图。在这个阶段，验证组不知道检查器（断言和覆盖）是否做了任何有用的事情或执行了所有的设计代码。
第三个维度提供了对检查器完整性的见解。这是一个定性维度，通过对测试平台进行彻底审查以及插入一些新bug来测试检查器是否正在检测出这些人为引入的bug来解决检查器的质量问题。
通常，通过好的设计和没有原生bug的情况下，验证工具可以构建证明，于是工程师便想知道为什么我们没有发现任何bug。为了解决这个问题，手动插入的bug提供了一种快速确定检查器是否合理的方法。此过程还有助于发现设计中的任何过度约束，这些约束可能会阻止在形式验证测试平台中注入合法有效的激励。这是称为过度约束分析的第四个维度，这是一种急需的定性评估，以发现潜在的关键测试平台bug。它为发现以前由于过度约束而未发现的新的设计bug铺平了道路。
第五个维度是一种工具驱动的自动化方法，用于发现在属性验证期间执行和达到哪些设计代码。这是一项按钮工具功能，可用于发现没有检查器或约束阻止代码可访问性的盲点。在此阶段发现标准代码覆盖率问题。
第六个维度称为场景覆盖，它提供了一个类似功能覆盖的定量视图，用于验证在处理功能执行的已知场景方面有多好。验证团队填充所需方案的电子表格，该工具会自动将它们合成为这些特定方案的断言和覆盖目标，并在形式工具中对其进行测试。它提供了面向视觉和指标的覆盖属性视图，并显示了这些特定场景的证明，因为知道这些场景经过了详尽的测试，因此毫无疑问地验证了这些场景。
IC设计验证的实用场所
来源：酷芯微电子
作者：ASHISH DARBARI
翻译：酷芯PR团队
校对：酷芯芯片验证团队