Btor2MLIR: A Format and Toolchain for Hardware Verification

想象一下你是一名试图破解谜题的侦探，但线索是用一种只有少数专家才能阅读的秘密代码编写的。在计算机科学的世界里，这种“秘密代码”就是描述计算机芯片（硬件）应当如何运行的语言。工程师们构建这些芯片来驱动从你的手机到太空卫星的一切设备，但如果设计中哪怕只有一个微小的错误，整个系统都可能崩溃或表现异常。为了防止这种情况，研究人员使用了“形式化方法”（formal methods）——这是一种数学工具，充当了超级强大的拼写检查器，旨在设计被制造出来之前就证明其完美无缺。

长期以来，这些拼写检查器一直说着不同的语言。有些说着“BTOR2”，这是一种在硬件竞赛中流行的格式；而另一些则说着“LLVM-IR”，这是软件编译器用于检查代码的一种语言。这就像是一个翻译员只能将法语翻译成英语，而另一个只能将西班牙语翻译成英语。如果你想用一个法语翻译员去检查一本西班牙语的书，你会发现无计可施。每次你都必须从头开始构建一个全新的翻译器。这篇论文介绍了一个新的、神奇的翻译器，叫做 BTOR2MLIR。它位于中间，作为一个通用的桥梁，让硬件设计能够与软件工具进行交流，而无需每次都重新造轮子。

问题所在：方言过多，桥梁不足

在硬件验证领域，BTOR2 格式已成为描述电路的标准方式，用于像硬件模型检测竞赛（HWMCC）这样的比赛。可以将 BTOR2 想象成一种非常具体且高效的方言，用于描述数字电路如何计数、加法运算或检查错误。像 BTORMC 这样的工具是专门为读取这种方言而构建的，用于检查电路是否安全。

然而，软件验证的世界规模宏大且功能强大。像 SEAHORN 这样的工具是检查使用 LLVM-IR 语言编写的软件代码的专家。这些工具已经非常成熟，经过了像 LLVM 编译器基础设施这样庞大项目的数十年磨练。它们拥有内置的功能，用于优化代码、寻找漏洞和运行模拟。

问题在于，这两个世界很少进行交流。为了使用强大的软件工具来检查硬件设计，研究人员不得不编写定制的、一次性的翻译器。这就像每次都试图把方榫头塞进圆孔里一样。这些翻译器通常必须重新实现一些基础功能（比如如何处理数字或循环），而这些功能在软件工具中早已存在，从而导致了精力的浪费和潜在的错误。

解决方案：通用适配器 (BTOR2MLIR)

本文的作者，来自滑铁卢大学的 Joseph Tafese、Isabel Garcia-Contreras 和 Arie Gurfinkel，决定建造一座更好的桥梁。他们创建了 BTOR2MLIR，这是一个基于 MLIR（多级中间表示）的新格式和工具链。

要理解 MLIR，请把它想象成一套巨大的、模块化的乐高积木。你不需要每次想建不同类型的房子时都从零开始建造一整座城堡，MLIR 提供了一套基础积木（方言），你可以将它们拼接在一起。你可以定义一个新的“硬件”积木，它的外观和行为看起来完全像 BTOR2，但它可以直接卡入现有的“软件”乐高结构中。

以下是他们的这个新工具是如何工作的：

1. 翻译器： 他们在 MLIR 内部构建了一个“BTOR 方言”。这是对 BTOR2 格式的一种直接、无损的转换。如果你有一个 BTOR2 文件，BTOR2MLIR 可以立即将其转换为这种 MLIR 方言。
2. 桥梁： 由于 MLIR 设计之初就具有可扩展性，他们创建了一个“转换过程”（conversion pass），将他们的 BTOR 方言转换为标准的 LLVM 方言。这是神奇的一步。它将硬件描述转化为软件工具（如 SEAHORN）能够原生理解的格式。
3. 结果： 输出结果是 LLVM-IR，这是一种软件验证引擎可以轻松吸收并进行分析的语言。

实验：它真的有效吗？

团队不仅建造了这座桥，还开着一辆卡车驶过以测试其承重能力。他们选取了来自 HWMCC 竞赛（具体为 2020 年和 2019 年的数据集）的一组真实世界硬件基准测试，并通过了他们的新工具链。

首先，他们检查了正确性。他们将一个 BTOR2 文件转换为其 MLIR 格式，然后又将其转回 BTored 格式。他们对比了原始文件和往返转换后的文件。结果如何？它们是完全一致的。安全性属性（电路必须遵循的规则）得到了完美的保留。即使在原始工具超时或耗尽内存的棘手案例中，他们的往返版本有时也能解决问题，这表明转换过程并未引入任何错误。

接下来，他们测试了性能。他们将该工具连接到著名的软件模型检测器 SEAHORN 以及快速求解器 BOOLECTOR。他们将这种新的“混合”流水线与专门为 BTOR2 构建的金标准工具 BTORMC 进行了对比。

结果令人惊喜且令人鼓舞：

• 速度： 在许多情况下，这种混合流水线（BTOR2MLIR + SEAHORN + BOOLECTOR）与专用的 BTORMC 工具相比具有竞争力，有时甚至更快。例如，在“19/mann”类别的基准测试中，混合方法在约 3,190 秒内解决了 44 个实例，而 BTORMC 在更多实例上耗时更长或超时。
• 灵活性： 该工具成功处理了诸如除法和位向量等复杂操作，证明了 MLIR 的“乐高积木”可以处理硬件逻辑中的繁重任务。
• 局限性： 作者坦诚地说明了目前工具无法胜任的地方。它目前支持位向量和数组，但尚未处理“公平性”（fairness）和“正义性”（justice）约束（即关于系统在无限时间内如何行为的规则）。此外，虽然它表现出色，但并未在每一个类别中完全碾压专门的硬件工具；它是一个强有力的竞争者，而非完全的替代品。

为什么这很重要

本文并不声称已经解决了所有的硬件验证问题。相反，它提出了一个全新的思考方式。通过使用 LLVM 编译器（驱动着从视频游戏到 Web 浏览器的各种工具）这一成熟且强大的基础设施，硬件研究人员可以停止重复造轮子。

作者展示了你可以将一个硬件设计转化为一种通用语言，然后使用强大的现有软件工具来检查它。这为快速原型设计打开了大门。如果研究人员想要尝试一种新的验证技术，他们不需要构建一个全新的引擎，只需要将想法接入 MLIR 框架即可。

未来，团队计划将这座桥梁连接到更多的工具，例如 KLEE（一种符号执行引擎）和 LIBFUZZER（一种模糊测试工具），这些工具目前用于软件，但可以彻底改变我们在硬件中发现漏洞的方式。他们还计划生成其他格式，如 AIGER 和 SMT-LIB。

最终，BTOR2MLIR 是一个概念验证，它表明硬件与软件验证之间的围墙正在倒塌。它表明，通过使用共同的语言，我们可以让我们的数字世界变得更安全、更快速、更容易构建。