技术只有在能改进既有方法论时才真正有用。属性生成仍在不断完善这一目标，但从长期看，它可能会非常有价值。

要点：

• 自上而下的半导体开发流程一直是芯片设计的目标，而“左移”正在让这一目标越来越可行。问题在于起点——规格说明——往往并不完整，甚至根本不存在，因为芯片行业长期以来在编写规格方面表现不佳。
• AI可以以多种方式嵌入现有流程。但“能做”并不意味着“该做”。这正是AI落地面临的重大挑战之一。许多现有任务都可以通过代理式流程更高效地完成，但这并不清楚是否就是正确做法。
• 当AI开始帮助处理过去一直很薄弱的环节——高质量、完整规格的创建——这一限制就会变得尤其明显。真正的问题是，AI能否让设计或验证环境自动从规格中推导出来。也许更准确的目标是：AI能否帮助创建更好的规格。有了更好的规格，下游设计就会容易得多。

“AI可以在几秒钟内生成一条SystemVerilog断言，”验证技术专家、图书作者Ben Cohen说，“但这条断言是否有意义，完全取决于它是从什么生成出来的，而在实践中，这个来源很少是单一、清晰、自然语言的规格。它往往只是一个含糊的段落，在被信任之前还需要澄清。”

解决这个问题应被视为高优先级。“现代SoC设计日益增加的复杂度，使得AI辅助的工件生成和验证收敛，已经从研究选项变成了现实需求，”南安普敦大学AI与EDA研究员Simon Davidmann说，“验证问题在实践中已经大到没有AI辅助就无法应对。处理器开发中验证工程师与设计工程师5比1的比例，并不是劳动力规划上的异常，而是复杂度已经超出既有方法能力的信号。”

从规格到任何结果，今天都还不是现实。“如果我们真的要把这件事变成现实，就需要在编写规格方面更有纪律性，”Synopsys应用工程总监Ravindra Aneja说，“如果我们真想让它成为现实，就必须去做。作为一个行业，我们准备好了吗？没有，我认为我们还没有到那个阶段。我不认为我们已经到了这样一个地步：无论是启动一个新设计，还是做一个衍生设计，你都可以说规格已经足够好了。”

我们甚至是否从正确的角度在思考这个问题？“一份散文式规格文档，形式化工具无法直接对其推理，因为形式化引擎处理的是精确、无歧义、可机器检查的陈述，而不是自然语言，”Axiomise首席执行官Ashish Darbari说，“AI能帮上的忙，是缩小这道鸿沟，更快地把散文转成候选的形式化陈述，而这实际上就是从规格中推导属性的含义。属性就是规格的形式化表达，而不是在那之后的另一个独立步骤。所以，与其把它理解为先规格、再属性、再形式化证明，不如更准确地说，属性集就是可机器读取的规格，而形式化是在完成这一步翻译之后对规格进行工作。”

有时，规格本身就是故意含糊的。“人类设计师会结合领域知识、过往经验以及提出澄清问题的能力来解释它们，”Davidmann说，“AI模型接收规格文本后会直接生成输出，却没有能力标记歧义或识别不一致。规格歧义很可能是LLM生成代码失败的重要原因之一，但现有研究文献尚未系统性地刻画它在多大程度上是根本原因，而不是模型能力限制。下一步应当是开发自动化规格分析方法，在歧义进入生成流程之前将其识别出来。”

是否应该从相反方向看待这个问题？“与其让形式化直接作用于规格，不如有充分理由认为，现代规格编写本身就应当从构造上做到形式化且可机器读取，”Normal Computing设计验证解决方案工程师Arvind Srinivasan说，“这是解决信任、覆盖和漂移这些内在问题的唯一方式。仅靠现有形式化方法结构上做不到这一点，但如果能使用新的求解器和像Lean这样的语言，就有可能实现。”

这可以服务于长期目标。“我希望把规格交给我的大语言模型，然后让它生成代码，”Cadence产品营销总监Paul Graykowski说，“但你如何捕捉规格的真实意图，并确保那就是你使用的唯一事实来源？还有很多事情必须被探索，很多现有规格都把这些事情视为理所当然。”

也许可以采用迭代式方法。“当你阅读RTL时，它可以给你一些关于RTL想要实现什么的抽象信息，”Synopsys的Aneja说，“它也许并不完美，但它可以给你一个不错的起点，然后你可以逐步修改那份规格。你可以从那里继续。它并不完美，但至少给了你一个合理的起点。”

技能迁移

自动生成属性被认为的一个优势，是它可能减少对专门验证人员的需求。但事实未必如此。

“对于没有内部形式化经验的团队来说，复杂的AI生成形式化属性可能会成为一个难以审查和维护的累赘，而且SystemVerilog断言方法的实用性边界是众所周知的，”Normal的Srinivasan说，“关键原则是内部一致性。高度依赖AI的设计流程，如何既把形式化作为对其他AI驱动设计和验证材料的检查，又利用其他材料来检查虚假或错误的形式化属性？把稳定的系统记录和内部一致性放在流程核心的用户，更适合以零信任方式使用这些系统。”

仍然需要有人逐条阅读每个生成的SVA属性。“他们需要判断前件是否过弱或过强，后件是否真正捕捉了实际需求，时钟和复位条件是否处理正确，以及该属性是否可能是空洞成立的，”Axiomise的Darbari说，“这要求既懂时序逻辑和断言语义，又深入理解微架构。没有这种能力，团队就无法分辨一个强属性和一个看起来很像、但实际上很弱的属性，也无法正确解读形式化工具的反例或‘已证明’结果。因此，现实中的要求是，AI可以减轻编写负担，但会提高流程中必须有懂形式化的工程师来解释和验证输出的重要性。采用这类工具的组织应当为这种专业能力预留预算，而不是假设工具会消除对它的需求。”

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

问题区域

空洞断言是一种需要直接关注的特定准确性风险。“空洞断言是一种SVA，它能正确编译，通过形式化工具，但实际上什么也没覆盖，因为无论设计做什么，它都始终为真，”Davidmann说，“空洞断言并不等于正确断言。一个能生成看起来合理、但实际上空洞的SVA的模型，会在消耗形式化工具能力的同时制造虚假的信心。那种在纸面上看起来准确、但在实践中极其危险的版本，就是模型自信且错误，测试平台也由模型生成，而流程中没有人具备足够的领域知识去发现问题。这不是假设中的失败模式，而是一种很容易在无意中构造出来的工作流。”

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

形式化验证涉及多种求解器，其中一种是模理论可满足性求解器（SMT）。它们用于判断一个数学公式是否可满足。“对于把形式化工具纳入流程的代理式系统来说，SMT求解器运行会带来不可忽视的成本，”Srinivasan说，“而且这类成本会随着设计复杂度和属性数量增加而上升。”

如何开始

决定如何把属性作为方法论的一部分引入，并不容易，需要考虑多个问题。也没有一种经过充分验证的单一方法论，因此每家公司很可能都需要自行摸索，找到技能、时间、算力投入与验证收敛程度之间的最佳平衡。

AI需要学会生成的属性将如何被使用。“有用于仿真的断言，也有用于形式化的断言，”Aneja说，“有一些技术可以让你写出更适合形式化的属性，这会帮助你在可扩展性上取得进展，也就是‘你能否根据属性的写法得到一个明确答案？’当你试图写这些属性时，与其写一条很长的属性，不如把这个功能拆成多个更小的部分。这样更具可扩展性。然后你就不会卡在一个需要200个周期才会出现有意义行为的场景上，因为那在形式化里行不通。”

“检索增强生成（RAG）提供了一种有原则的解决方案，”Cohen说，“与其完全依赖LLM训练时学到的内容，不如让一个增强了RAG的系统在生成时查询一个经过筛选的知识库——检索与当前任务相关的具体规则、模式和经验教训。RAG规则代表了多年积累的应用知识——这些规则来自真实项目、真实工具行为和真实失败。它们编码的不只是语法上正确的内容，还有可验证正确的内容；包括一个假设是恰当地约束了环境，还是让形式化证明空间变得不可达之间的差别；包括一个属性是否检查了正确行为，还是只是空洞通过；包括时序图是否与生成代码一致，还是在无声无息中偏离。”

还可以尝试分阶段的方法。“有一个中间步骤叫正式测试计划，如果你有一份完美的规格，它讲的是你的设计做什么，而不是你想验证什么，”Aneja说，“我的意思是，借助这些LLM和代理，你可以读取文本、查看时序图、查看FSM图以及你可能拥有的其他图像，然后根据你正在做的设计提取某些特征。你可以训练系统去判断：这是CPU设计吗？这是GPU设计吗？这是AI加速器吗？再往下一层，是内存控制器吗？是中断控制器吗？是总线桥吗？还是跨不同主设备和从设备的某种互连？根据这些内容，它可以提取出你可能想测试的某些特征。”

选择LLM时也要考虑同样的问题。“领域边界意识需要成为一门首要的工程学科，”Davidmann说，“在把任何AI模型引入生产流程之前，正确的问题不仅是模型有多准确，还要看它训练于什么、那个分布没有覆盖什么，以及实际设计离那个边界有多近。每个部署这些工具的团队都应该对一组具有代表性的、最复杂和最具新意的设计模式进行有意识的边界探测，并由领域专家独立核对输出。这个练习可以识别出分布的终点和模型不确定性的起点。没有它，部署就是在缺少管理风险所需信息的情况下推进。”

先从小处开始，建立信心。“先在一个范围明确、理解充分的模块上试点，把AI输出与现有手工编写的属性集进行比较，并在广泛推广前衡量差距，”Darbari说，“最后，这只有在与已经理解形式化方法的工程师一起使用时才会有效。它不是用来跳过这种专业能力的，而是用来让专家工程师更快。在这方面，我看到大型设计公司出现了一个有意思的需求。管理层希望工程师接受形式化训练，这样他们就能驱动整个工具生态，并正确应用方法论。”

同时，考虑你所处的领域也很重要。“当前工具已经领先于治理，”Davidmann说，“大多数团队还没有标准来记录哪些断言是人工编写的，哪些是AI生成的，或者这种区别对签核信心意味着什么。此外，大多数供应商文档也没有说明模型的训练范围、失败模式或部署模型的领域边界。在AI生成内容扩展到安全关键设计之前，这两个缺口都需要先补上。”