AI 自动生成属性（Properties）：从规范到验证的方法学插入分析

要点：

• 虽然 AI 可以根据规格说明编写属性，但如今现存的规格说明很少能好到从中生成任何有用的东西。
• 自动生成属性并不能减少对精通该语言的人才的需求，也不能减少对形式化工具的应用。
• 如今，将这一方法引入工作流程的做法可能因公司而异，目前尚无经过充分验证的方法论可供借鉴。

自顶向下的半导体开发流程长期以来一直是芯片设计的目标，而左移（shift left）无疑正使这一目标越来越有可能实现。问题在于，起点——规格说明——往往不完整甚至根本不存在，因为芯片行业在撰写规格说明方面一向表现糟糕。

有几种方法可以将 AI 引入现有流程。但能做并不意味着应该做。这是 AI 落地面临的重大挑战之一。许多现有任务可以通过智能体流程更高效地完成，但是否这样做才是正确的选择，尚不清楚。

当 AI 开始介入一项过去一直严重不足的工作——创建优质、完整的规格说明——时，这一局限尤为明显。最大的问题在于，AI 能否让设计或验证环境从规格说明中自动推导出来。也许一个更正确的目标是：AI 能否帮助创建更好的规格说明。有了更好的规格说明，下游设计就会容易得多。

“AI 可以在几秒钟内生成一条 SystemVerilog 断言，”验证技术专家兼图书作者 Ben Cohen 说。“但这条断言是否有意义，完全取决于它是从什么内容生成的，而实践中，其来源很少是一份单一、干净的自然语言规格说明。它往往是一段含糊不清的文字，需要先澄清才能被信任。”

解决这个问题应被视为当务之急。“现代 SoC 设计日益复杂，正使 AI 辅助生成工件和收敛验证从研究选项变为实际需求，”南安普顿大学 AI 与 EDA 研究员 Simon Davidmann 说。“实际上，验证问题的规模已经到了没有 AI 辅助就无法应对的地步。处理器开发中验证工程师与设计工程师 5 比 1 的人员配比，并非人力规划上的异常，而是一个信号：复杂度已经超出了现有方法的承载能力。”

如今，从规格说明生成任何东西都还不现实。“如果真要把这变成现实，我们在撰写规格说明方面需要更多的纪律性，”Synopsys 应用工程总监 Ravindra Aneja 说。“如果我们真心想实现它，就必须为此努力。作为一个行业，我们做到了吗？不，还没有。我认为，无论是启动全新设计还是做衍生设计，目前都还达不到可以说规格说明已经足够好的程度。”

我们的思考方式本身对吗？Axiomise 的 CEO Ashish Darbari 表示：“形式化工具无法直接对散文式的规范文档进行推理，因为形式化引擎处理的是精确、无歧义、机器可校验的语句，而不是自然语言。AI 能帮助的是缩小这一差距，更快地把散文翻译成候选的形式化语句——这实际上就是从规范中提取属性在实践中真正要做的事情。属性就是规范的形式化，而不是规范之后的独立步骤。因此，与其把它看作先有规范，再有属性，然后进行形式化证明，更准确的说法是：属性集就是机器可读的规范，一旦这种翻译完成，形式化方法就是在直接处理规范本身。”

有时候，规范是有意保持模糊的。南安普顿大学的 Davidmann 说：“人类设计师依靠领域知识、过往经验以及提出澄清问题的能力来解读规范。AI 模型接收规范文本后直接生成输出，却没有标记歧义或发现不一致的能力。规范中的歧义很可能是 LLM 生成代码失败的一个重要原因，但目前的研究文献尚未系统性地刻画这种情况在多大程度上是根本原因，以区别于模型能力本身的局限。下一步是开发自动化的规范分析方法，在歧义进入生成流水线之前就把它识别出来。”

这个问题是否应该反过来看待？Normal Computing 的设计验证解决方案工程师 Arvind Srinivasan 说：“与其让形式化方法直接处理规范，一个更有力的观点是：现代的规范编写应该从构造上就是形式化的、机器可读的。这是解决信任、覆盖率和偏差这些固有问题的唯一途径。仅靠现有的形式化方法学在结构上是不可能做到这一点的，但如果你能使用 Lean 这类新颖的求解器和语言，就有可能实现。”

这可以服务于长期目标。Cadence 产品营销总监 Paul Graykowski 说：“我想把一份规范交给我的大语言模型，让它生成代码。但你要如何捕捉规范真正的意图，并确保它就是你作为唯一事实来源所使用的东西？有很多东西需要探索，这些是现有规范习以为常、被默认成立的东西。”

迭代式的方法可能有其用武之地。Synopsys 的 Aneja 说：“阅读 RTL 时，它可以给你一些关于你的 RTL 想做什么的抽象信息。它可能不完美，但可以给你一个很好的起点，然后你可以以增量的方式修改那份规范。你就可以由此继续下去。它并不完美，但至少给了你一个合理的起点。”

技能迁移
自动生成属性的一个所谓优势是，它能减少对专业验证人员的需求。但实际情况可能并非如此。

Normal 公司的 Srinivasan 表示：“对于缺乏内部正式专业知识的团队来说，审查和维护复杂的 AI 生成的形式化属性可能是一项吃力不讨好的负担，而且 SystemVerilog 基于断言的方法学的效用边界是众所周知的。关键原则是内部一致性。高度依赖 AI 的设计流程如何将形式化方法用作对其他 AI 驱动的设计和验证产物的检查，同时又利用其他产物来检查形式化属性是否虚假或错误？那些把稳定的记录系统和内部一致性置于流程核心的用户，将更有能力以零信任的方式利用这些系统。”

仍然必须有人去阅读每一条生成的 SVA 属性。Axiomise 的 Darbari 说：“他们需要判断前件是否太弱或太紧，后件是否捕捉到了实际需求，时钟和复位条件是否处理正确，以及该属性是否可能空洞地通过。这要求精通时序逻辑和断言语义，同时对微架构有深入理解。没有这些技能，团队就无法区分一个强属性和一个碰巧看起来相似的弱属性，也无法正确解读形式化工具给出的反例或‘已证明’的结果。因此，实际要求是：AI 降低了编写负担，却提高了让具备形式化素养的工程师参与其中来解读和验证输出的重要性。采用这一技术的组织应当为这种专业知识做好预算，而不是想当然地认为工具可以免除这一需求。”

有些角色可能比其他角色更能从形式化属性中获益。Ashley Stevens 是 Arteris 的产品管理与营销总监，他说：“形式化验证正在成为解决方案中越来越重要的一部分。它在架构合规性方面尤其强大——确保 ISA 属性对所有合法的指令序列都成立——并在实现验证中用于强制硬件协议的正确性。但形式化方法并不能取代动态验证或系统级验证，尤其是涉及完整的 SoC 行为和真实工作负载时。在实践中，形式化方法起到的是补充作用，用于证明深层边界情况下的正确性，而仿真和模拟则用来确立端到端的完整性。”

问题领域
空洞断言是一种值得直接关注的特定准确性风险。“空洞断言是一条能正确编译、能通过形式化工具、却什么也没覆盖的 SVA，因为无论设计做什么它都恒为真，”Davidmann 说。“空洞断言不等同于正确的断言。一个生成看似合理却空洞的 SVA 的模型，在消耗形式化工具容量的同时提供虚假的信心。这种技术在纸面上看起来准确、在实践中却真正危险的情形是：模型自信且错误，测试平台也是由该模型生成的，而流程中没有人具备发现问题的领域知识。这并非假设性的失败模式，而是一种很容易在无意中构建出来的工作流。

它们伴随着高昂的成本。Cohen 说：“在正式验证流程中，这类错误的代价很高。它们消耗工具运行时间、工程师的调试时间，而且——最关键的是——会侵蚀人们对验证结果本身的信心。”

形式验证涉及多种类型的求解器，其中之一是可满足性模理论（SMT）求解器。它们用于判定一个数学公式是否可满足。Srinivasan 说：“对于将形式化工具纳入闭环的智能体系统来说，SMT 求解器的运行会产生不小的成本。此外，这些成本还会随着设计的复杂度和属性数量的增加而扩展。”

入门指南
如何开始将属性作为方法论的一部分来使用，并不显而易见，而且有几个问题必须加以考虑。目前也没有一种经过充分验证的单一方法论，很可能每家公司都需要自行摸索，找出在技能、时间和算力投入之间达成最佳平衡、并实现最高程度验证收敛的方案。

AI 需要学习生成的属性将如何被使用。Aneja 说：“有用于仿真的断言，也有用于形式验证的断言。有一些技巧可以编写对形式验证友好的属性，这有助于你在扩展性方面受益，比如‘能否根据属性的编写方式得到确定的答案？’在编写这些属性时，与其写一个非常长的属性，不如把那个功能拆分成多个更小的部分。这能带来可扩展性。这样你就不会卡在一个需要 200 个周期才能产生有意义结果的行为上，因为它在形式验证中行不通。”

Cohen 说：“检索增强生成（RAG）提供了一种有原则的解决方案。RAG 增强的系统不再仅仅依赖 LLM 在训练中学到的内容，而是在生成时查询一个经过精心整理的知识库——检索适用于当前任务的特定规则、模式和经验教训。RAG 规则代表着多年积累的应用知识——这些规则源自真实的项目、真实的工具行为和真实的失败。它们编码的不仅是语法上正确的内容，更是可验证有效的内容；是恰当地约束环境的假设与让形式证明空间无法企及的假设之间的区别；是检查正确行为的属性与空洞通过的属性之间的区别；是与生成代码相匹配的时序图和悄然而悄然偏离的时序图之间的区别。”

有一些循序渐进的方法可以尝试。Aneja 说：“有一个中间步骤叫做形式验证测试计划，如果你有一份完善的规格说明，它描述的是你的设计做什么，而不是你想验证什么。思路是，借助所有这些 LLM 和智能体，你能够阅读文本、查看时序图、查看 FSM 图以及可能拥有的其他图片，然后你可以根据正在做的设计提取某些特征。你还可以训练你的系统去判断：这是一个 CPU 设计吗？是一个 GPU 设计吗？是一个 AI 加速器吗？再往下看一层，它是一个内存控制器吗？是一个中断控制器吗？是一个总线桥吗？还是某种横跨不同管理者和从属者的互连？根据判断结果，它就可以提取出你可能想要测试的某些特征。”

选择 LLM 时也需要同样的考量。“领域边界感知需要成为一流的工程学科，”Davidmann 说。“在将任何 AI 模型引入生产流程之前，正确的问题不仅是模型的准确度有多高，还包括它是基于什么训练的、该训练分布未覆盖哪些内容，以及实际设计与该边界的接近程度。每个部署这些工具的团队都应该在其最复杂和新颖的设计模式的代表性样本上进行一次审慎的边界探测演练，并对照领域专家的产出独立验证输出结果。这项演练可以确定分布在哪里结束、模型的不确定性从哪里开始。没有它，部署就是在缺乏管理风险所需信息的情况下进行的。”

从小处着手，逐步建立信心。“先在一个边界清晰、理解透彻的模块上进行试点，将 AI 输出与现有的手写属性集进行对比，并在广泛推广之前衡量差距，”Darbari 说。“最后，这只有在与已经理解形式化方法的工程师配合时才能奏效。它不是跳过该专业知识的捷径，而是让专家工程师更快的方法。这是我看到大型设计公司提出有趣需求的一个领域。管理层希望培养具备形式化方法能力的工程师，以便他们能够驾驭整个工具生态系统并正确应用方法论。”

同样重要的是，要考虑你所处的领域。“工具的发展目前领先于治理，”Davidmann 说。“大多数团队还没有制定标准来记录哪些断言是由人类编写的、哪些是 AI 生成的，以及这种区分对签核置信度意味着什么。此外，大多数供应商文档并没有说明所部署模型的训练范围、失效模式或领域边界。在 AI 生成的内容扩展到安全关键型设计之前，这两个缺口都需要弥合。