形式验证技术的进展

专家在座：半导体工程与 Axiomise 首席执行官 Ashish Darbari 坐下来讨论形式验证工具和方法的进步;张瑾，Cadence 验证组产品管理组总监;新思科技研发执行董事 Sean Safarpour;以及西门子 EDA 数字验证技术首席工程师 Jeremy Levitt。以下是该讨论的摘录。

从左到右：Axiomise 的 Darbari;Cadence 的 Zhang;新思科技的 Safarpour;和西门子的莱维特。

SE：当有初创公司时，我们听到了很多关于形式验证的进步，但当大型 EDA 公司内部进行开发时，我们听到的就更少了。这里正在取得哪些技术进步？

莱维特：这些都是指数级的问题，所以有足够的空间来提高性能。有些地方存在不连续性，并且出现了新的算法。但即使没有这一点，从一个版本到另一个版本，从年复一年，你会看到这些工具的速度提高了 25% 到两倍。我们看到性能呈指数级增长。当然，设计会越来越大，你在这里玩的是一个非常困难的追逐游戏。但是工具的性能有了显着提高。这有时是由于启发式方法的调整、应用机器学习来找出更好的参数设置或更好的调查领域。这部分是由于使用了云，其中有额外的计算资源可用，这允许您并行执行许多作。我们开始看到法学硕士的应用带来一些改进，但这在未来可能比今天的工具更多。

Safarpour：初创公司确实会发出很大的噪音。我们已经有一段时间没有在纯形式验证领域有初创公司了。使用正式的人们看到了大量的创新、巨大的影响以及他们可以解决的问题类型的扩展。谁使用正式验证的情况发生了巨大变化。其中许多公司都表明，形式化验证可以在发现错误和签核方面增加很多价值。我想谈谈 SAT 比赛。SAT求解器是形式化验证的主要基础求解器之一，SAT竞赛已经存在了大约20年。每隔一段时间，就会出现一个新的 SAT 求解器。有 Chaff 和 zChaff。这是开创性的，人们说这对于 NP 完全问题来说可能是最好的。然后 MiniSAT 出现了。这些事情发生了，然后有一段时间，即使是 SAT 专家也会说事情平静下来。但如果你回到五年前，kissat，MapleSAT，很多新的求解器即将到来。如果你看看 SAT 比赛和最近的成绩，他们只是把前一年的成绩从水面上吹了出来。从求解器的基本层面一直到应用链，仍然有很多创新正在发生。即使在这个基本层面上，仍然有很多创新正在发生。一些最新数据还显示了人工智能如何帮助改进许多此类 SAT 求解器算法。这非常令人兴奋，而且有很多动作。对于社区之外的人来说，这很难看到，但我认为在这个地区是一个非常激动人心的时刻。

张：Jasper（Cadence 旗下）在市场上仍然非常成功。大家的努力让研发团队在开发新技术方面保持警惕。其中很多都是在引擎层面的幕后进行的。这些是用户可能看不到的改进。我们的理想目标不是给他们很多旋钮让他们调音，而是给他们编排，让他们更容易使用正式的。这是多年来最大的挑战。技术改进、SAT 求解器和云、分布式计算——所有这些事情都在发生。所有公司都投入了大量资金，只是为了在竞争中保持平起平坐或领先。

Darbari：所有 EDA 公司都在生产出色的工具，这让像我们这样的人在该领域看起来很聪明。最近完成的很多工作都是在 SAT 求解器中完成的。作为形式化工具的用户，我们看到它们在证明收敛率方面发挥了很大的作用。但让我退后一步，描述定义正式用法的五个关键领域。第一个是财产生成。谁编写了这些属性，这些属性有多好？除非它们是标准协议，否则它们不会在以太中发明。如果它们与规范挂钩，那么房间里的大象问题就是，“你如何将复杂、庞大的规范转化为有意义的属性？除非你具备这一点，否则你实际上无法用形式来解决功能验证问题，尽管许多应用程序驱动的形式仍在继续使用并且正在产生很大的影响。除非我们开始通过与规范建立更好的联系来在功能空间中采用形式化，并使属性生成更快、更好、更高效，否则我们实际上无法在形式化方面产生太大的影响。效率带来了另一个相关的挑战，即约束细化并确保正确捕获约束并有效地对其进行建模。一旦完成了这两件事——例如，编写断言并充分模拟假设以确保正确性和效率——那么如果它们失败，您将面临第三个挑战，即调试。工具中发生了很多事情。然后你想谈谈房间里的下一头大象，这就是证明收敛。我们如何让这些事情变得更好更快？设计复杂性不断增加数倍，因此总有追赶工作要做。但是，然后是签字和报道，以及如何全面解决故事的所有最后部分，以确保所有经过正式验证的内容实际上都正确完成，芯片中没有留下任何错误等等。从用户的角度来看，这种转变正在朝着解决方案层的定制化方向发展。这也是我们做很多工作的地方。客户现在以一种他们以前没有感知到的方式看到正式。例如，如果您谈论的是 RISC-V，我们已经做了很多定制解决方案工作。我们从中发现了好处。十年前，如果你去找某人说你可以用正式的详尽地验证一个有序处理器或无序处理器，他们会嘲笑你。这不是他们能想到的。但今天我们可以做到这一点。它是求解器和有效编写属性的应用程序工程师的组合。许多正式的正在悄悄地在验证的各个方面发挥作用。我只谈到了功能性，但它在其他方面也产生了巨大的影响。

Jeremy：我的第一个答案是关于发动机的性能，它肯定呈指数级增长。但 Ashish 提出了一个很好的观点，即改进的使用模型以及这些工具允许用户访问这种能力的难易程度。我们看到工具方面的持续创新，使用户更容易指定他们想要的东西，就工具需求进行沟通，并改进整体流程，以便更广泛的客户和知识水平可以更有效地使用这些工具。

张：如果我回顾过去 20 年，一路上有哪些重大变化真正将正式推广到更广泛的用户群？SystemVerilog 断言的标准化是其中的关键部分，形式化作为一种技术在不同领域的扩散。围绕工具创建的特定于应用程序的解决方案有助于找到可以使用正式的所有不同用例，也许没有专业知识。这是一次伟大的冒险，它扩大了正式应用范围。另一个想到的是正式签字。在此之前，正式一直被视为一种调试工具。如果你不能在一个块上签字，它就会成为一个可有可无的，也许不是必备的。但是，一旦你能够进行签核和有限制的签核，当你有了一种真正帮助人们从更严肃的角度看待正式的方法时，你就可以真正在流程中部署它。最近，随着机器学习的注入，以及最近的 GenAI，正在发生的许多事情都是重要的里程碑，将正式视为验证流程的一部分。如今，我们必须做的宣教推销少了很多。研发团队正在进行的幕后所有其他事情——标准化、方法论——都有助于正式化。这确实是当今每家公司都在使用的主流工具。

SE：我们听到了很多关于数据中心进步、CXL 和 HBM 等新技术的信息。正式版一直受到它需要的内存量和计算量的限制。从理论上讲，现在我们拥有无限的内存和无限的计算。这对正式有多少帮助？

Levitt：这些新架构可靠地为您提供了线性加速，但问题是指数级的，或者至少是 NP 困难的。我们会接受这一点，但我仍然想说大部分进步是由 SAT 求解器的改进推动的。这些正在呈指数级增长。与我们运行的算法以及我们如何编排它们相关的工程改进也呈指数级增长。提高计算能力，我们会接受这一点，但这是一种线性加速，如果它能让你同时做更多的事情，有时是超线性的。但真正的性能改进仍然来自基本的 SAT 求解器级别和算法级别，而不是来自资源可用性的增加。

Darbari：除了 SAT 求解器的效率之外，你如何对事物进行建模也会对抽象产生重大影响。我有一个很好的例子，来自我们最近在 DVCon India 上展示的工作，关于 RISC-V 处理器。它有一个五到六级的深度管道，在一台具有 1.5 TB RAM 和 96 个内核的机器上运行。我们得到了 10,331 个曲柄的有界证明。试图证明“add”指令的一个实例可以在管道中发送并且实际上可以正确执行。不要介意整个指令空间，只需一条“添加”指令。然后，我们完成了分解它并引入覆盖率分析和抽象引擎的过程。然后，我们能够在大约 100 秒内证明相同的属性，界限为 18。我们无法更早地证明这一点的唯一原因是处理器中存在活锁。我们开始寻找它，因为这是一个 NP 难题，所以我们试图一次性验证作数的所有实例和所有情况。如果这些案例中的任何一个遇到驼峰，则证明被卡住。你可以把最大的机器扔给它，但你实际上无法有所作为。一直使用正式的人都明白这一点。我能在较小的机器上获得相同的结果吗？在这种情况下，当我们确实在具有 18 GB RAM 的 128 核机器上放置相同的测试平台时，我们也得到了证明，只是花费的时间有点长。计算会有所作为，但它是渐近的，除非我们了解正在验证的内容以及如何建模，否则在问题上投入更多计算不会产生重大影响。

Safarpour：如果我们从用户的问题角度来看，Ashish 说的是一个难以证明的单个属性的问题，而且总是有这样的案例。但我们看到的是，问题的巨大规模，以及他们试图解决的财产的绝对数量，比前几代人要大几个数量级。从我们的客户那里听到，在正式的财产验证设置中，而不是连接或覆盖范围或类似的东西，他们有数十万甚至数百万的财产需要证明，这并不少见。在这些设置中，计算会产生很大的不同。如果您有数百个可用内核或数千个可用内核，那么您可以做很多事情。虽然证明一处房产总是很困难，但我们发现自己必须解决的挑战之一是管理。您拥有数十万个属性，您有数百个核心可供您使用。即使您每晚运行回归或一周以上，有些属性也没有足够的时间让任何单个引擎对其进行处理。你必须创新，因为在过去，你不会遇到像现在这样广泛的问题。我们的客户为我们带来的大量产品已成为一项重大挑战。机器可用性是存在的，但我们需要在编排和智能部署方面做的事情确实起着至关重要的作用。客户确实会来找我们问，'如果我给你 10,000 个内核怎么办？如果我给你 100,000 个核心几个小时怎么办？你能破解这个吗？它正在打开这个大规模并行的领域。这很棒。问题越来越难了。计算可用。这使我们能够解决这些新问题。

张：从工具的角度来看，我们肯定希望利用并行化，利用所有的计算。但现实情况是，客户没有无限的计算能力。我们仍在努力工作，即我们能为您提供的计算量有限，并且我们正在与模拟和所有其他工具竞争。存在现实生活中的限制，但在技术方面，有很多进步正在利用我们可以做的事情来并行化作业，以最有效的方式编排作业，利用以前的结果。所有这些改进都是从工具的角度出发的。但我希望我们有无限的计算能力。