Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement

在微芯片这个隐形的世界里，数十亿个晶体管通过开启和关闭来为从智能手机到航天器的各种设备提供动力，而一个隐藏的错误就可能导致系统发生灾难性的故障。工程师们使用一种称为寄存器传输级（RTL）的语言来设计这些芯片，这种语言描述了数据如何在存储元件之间随时间移动。为了确保这些设计在制造前能够正确运行，验证专家会编写“断言”（assertions）。可以将断言想象成写在设计本身中的一条严格规则，它表达了这样一种观点：“如果发生了这件事，那么必然会随之发生那件事。”如果芯片违反了这条规则，系统就会发出警报，揭示出那些可能被忽略的漏洞。几十年来，编写这些规则一直是一项缓慢、手动且易出错的任务，需要工程师去猜测哪些行为可能会出错，并为它们编写特定的检查机制。虽然计算机可以通过挖掘现有的设计仿真来寻找模式以提供帮助，但这些自动化方法往往会错过最危险的情景，仅仅是因为它们所依赖的随机测试永远无法偶然撞见这些情景。

来自香港科技大学（广州）的一个研究小组开发了一种解决该问题的新方法，并将其系统命名为 NeuroAssertion。该方法并不依赖于随机机会来寻找漏洞，而是主动搜寻芯片设计中最难触及的行为，然后结合人工智能与形式逻辑来编写必要的安全规则。该过程始于对设计进行转换，以便更容易观察正在测试的部分。研究人员在代码中插入特殊的标记，以追踪特定的、难以触发的条件是否曾经发生过。随后，他们使用一个被称为“模型检测器”的强大数学引擎，强制设计执行这些罕见的条件。这生成了一组高度特定的测试用例，能够暴露那些随机仿真可能永远无法发现的行为。这些全新的、多样化的轨迹为下一步提供了更丰富的基石。

一旦系统获取了这些难以发现的行为，它就会进入生成阶段。它使用一种称为“语法引导合成”的技术，基于观察到的数据创建初始安全规则。然而，研究人员意识到第一轮尝试很少是完美的。为了解决这个问题，他们引入了一个充当严谨编辑的角色——精炼循环。系统通过向代码中注入被称为“变异体”（mutants）的小型刻意错误，来衡量当前规则集检测设计变化的能力。如果规则未能捕捉到变异体，系统便能准确知道哪个行为仍未被检查。随后，它会调用大语言模型，提出专门旨在覆盖该空白点的全新规则。如果提出的规则存在逻辑缺陷，第二个语言模型并不会将其丢弃；相反，它会分析错误，并构建一套专门的指令或“文法”，以引导符号求解器修复该规则。这创造了一个循环，使系统不断提出、检查并修复断言，直到它们既丰富又稳健。

该方法的成果在七种不同的芯片设计上进行了测试，范围涵盖了从小型仲裁电路到复杂的处理器核心。这一新框架的表现始终优于被称为 SMART 的现有最先进方法，后者依赖于没有这种主动精炼过程的单次挖掘。在这些实验中，NeuroAssertion 生成的断言数量大约是旧方法的两倍。更重要的是，这些规则的质量显著提高。通过衡量其检测注入错误的能力，新系统实现的变异覆盖率约为传统方法的两倍。在某些特定的基准测试中，这种提升甚至更加剧烈；例如，在一个处理器组件上，变密覆盖率从大约 6% 跃升至 32% 以上。研究人员还将他们的系统与一种直接方法进行了对比，即在没有任何形式检查或精炼步骤的情况下要求大语言模型编写规则。直接方法产生的规则要少得多，且未能捕捉到大多数潜在错误，这证明了仅靠原始的语言生成对于这项高风险任务而言是不够的。

通过将断言生成视为一个持续探索与精炼的循环而非一次性事件，研究人员展示了自动化创建复杂硬件高质量安全规则的可能性。该系统不仅仅是在猜测；它主动寻找设计的盲点，并利用神经网络与形式逻辑之间的协作来填补这些盲点。这项工作表明，硬件验证的未来在于将人工智能的模式识别能力与数学证明的严谨确定性相结合，从而确保驱动我们世界的芯片能像设计它们的工程师一样可靠。