形式化验证领域长期以来面临一大难题：属性编写困难。尽管相关语言标准已存在数十年，工具也持续改进，但这一障碍从未真正消除——而AI或许正在改变这一局面。
AI具备读取自然语言文档并从中提炼信息的能力。一个极具实用价值的应用方向，便是读取规格说明并自动生成一组属性，用于验证实现是否与规格说明相符。然而，这一过程存在多重挑战，也潜藏着不少陷阱。
SystemVerilog语言中有一部分专门用于对设计属性进行形式化定义。当这些属性应用于验证环境时，被称为断言。属性定义了信号之间的逻辑与时序关系，使协议等内容得以明确表达。一组属性应能定义设计中全部预期行为，且不与这些行为的具体实现方式相耦合。从这个意义上说，属性构成了一种规格说明，可据此判断RTL实现是否正确。
然而，SystemVerilog断言（SVA）语言并不易学，尤其是其声明式的语言特性——与设计和验证流程中大多数环节所使用的面向对象过程式语言截然不同。多年来，业界一直尝试开发工具和方法论以简化属性编写。近期，基于大语言模型的工具已取得显著进展，尽管仍有若干突破有待实现。
其中一项近期突破是知识图谱的创建，由Cohen和Chibani提出。知识图谱以"事物及其关系网络"的形式存储信息，而非平面文本。它由三部分构成：节点（实体，如信号、模块、需求、端口）、边（关系，如驱动、复位、响应、归属），以及以"主体→关系→对象"形式存储的三元组。
知识图谱充当一个可快速访问的信息数据库，无需每次都依赖大语言模型重新提取。普通的检索增强生成（RAG）检索的是看起来相关的文本片段，而知识图谱检索的是具体事实及其关联关系。正因如此，基于知识图谱的框架能提供更好的事实依据——由于关系被显式存储，模型编造信号名称或误读关系的可能性大幅降低。
讽刺的是，一个重大问题恰恰在于找到一份充分的规格说明。Synopsys应用工程总监Ravindra Aneja表示："理想情况下应有一份完美的规格说明，但至少在过去30年里这从未实现。大多数情况下不会有完美的规格说明，有时甚至根本没有。这取决于是否是新设计还是衍生设计、是谁在编写，以及属于哪个组织。但在AI出现之前，编写完美规格说明或文档并不是一件'时髦'的事。人们往往在填写规格说明之前就已经开始设计，因为他们脑海中已经有了想法。随着AI的出现，人们开始更加重视这件事。"
目前已能实现相当多的功能。Axiomise首席执行官Ashish Darbari表示："AI可以读取规格说明文档、协议标准，甚至RTL注释，并提出第一轮断言草案，涵盖复位、握手、独热条件以及明显的安全检查。对于不经常变更的标准规格说明，这一过程能够加快编写样板SVA这一繁琐环节的效率。"
这一需求早已存在。Siemens EDA高级副总裁兼总经理Abhi Kolpekwa表示："人们认为，读取规格说明并将其转化为其他有形成果，是AI很适合解决的问题。但这也需要变更管理能力，因为规格说明很可能会发生变化。要在验证流程中实现变更管理，需要在智能体之外做更多的工作。这被称为情境智能——我们需要创建情境和情境智能，不仅能理解变更内容，还能结合历史与验证流程的可能未来做出更明智的决策。"
规格说明从来都不是一成不变的。Aneja补充道："我在边梳理规格说明边进行开发，但市场部门可能突然要求增加某个新功能，于是你又回头修改规格说明。有时偏差可能是小的，有时可能是重大的。无论做了什么更改，如何在设计和验证环境中体现出来？AI在这方面很擅长，能判断偏差所在及其对验证的影响。业界正在广泛讨论如何管理这种基于变更的设计流程，这正是AI大有用武之地的地方。"
前方危险
规格说明是否完整？Darbari表示："完整性是另一个完全不同的问题。现实中的芯片开发很少是孤立进行的。即便是全新项目，也很少会有完整的规格说明涵盖所有微架构和架构细节，包括通常是Bug重灾区的接口部分。以我的经验，AI生成的属性集在结构性和语法覆盖方面表现强，但在架构意图和规则背后的'原因'方面较弱。因此，AI的实用价值是真实的，但完整性必须通过独立手段加以验证，通常需要一位充分理解设计意图、能够判断遗漏内容的工程师来完成。"
所有信息是否都被采用？Normal Computing设计验证解决方案工程师Yaron Ilani表示："这些断言的实用性和完整性，取决于AI引擎的能力以及其对规格说明细微差别的理解准确度。在Normal，我们通过运行'自动形式化'并生成本体论来应对这一挑战。潜在风险包括因规格说明存在空白或歧义而导致的错误假设，这些风险可以通过在前期运行规格说明审查步骤来加以缓解。"
两类问题都可能导致属性集不完整。Darbari指出："最大的危险是虚假的信心。团队获得大量属性，通过形式化工具运行后看到绿色验证结果，便将其视为已完成签核。但证明的质量取决于属性的质量，一个薄弱或空洞的属性可以轻易通过，而实际上什么有意义的内容都没有被检查。AI生成的属性尤其容易出现这种问题，因为模型可能生成语法上有效但逻辑上过于宽松的SVA——前置条件缺失或过度约束，或者检查了错误的信号关系——而这些仍然能通过编译和检验。"
这本身也变成了一项验证任务。Normal产品经理Hanna Yip表示："从规格说明中推导属性，需要将非结构化的多模态信息提炼为可证明的命题。虽然提取过程本身可以高效进行，但确保所提取内容的正确性相当具有挑战性。"
过去，验证的发生方式是：设计团队解读规格说明，验证团队也解读规格说明，然后两者的解读结果相互比对——这一过程有时还能发现规格说明本身的问题。Darbari表示："生成的属性可能悄然将AI对规格说明的误读当作事实固化下来。解读错误被嵌入看似严谨的产出物中。还存在规模化风险：如果这些属性进入下游FMEDA、安全案例或ISO 26262/ISO 21434认证证据，一个未被察觉的缺口就不会只局限于一个项目。"
这也意味着，你无法完全信任AI的输出。Normal产品设计负责人Kaye Mao表示："信任是一个大问题。如何验证不是你自己做的工作，尤其是当智能体对自己的正确性极度自信，且被训练成能够通过粗略检验时？例如，你如何验证一个测试实际上是在按规格说明测试设计？你是否需要查看实际波形？这本身就耗时，因此可能需要新颖的方式来检验智能体的工作成果。"
鉴于近期AI失控的相关事件，Mao还提出了另一潜在隐患："另一个危险是未能限制智能体在执行特定任务时可访问的附属资料。智能体只要有机会就会'走捷径'。例如，它们可能利用设计本身来生成测试用例，这违背了保持验证与设计相互独立的初衷。"
投资回报率
AI显然能够完成这项任务的某些环节，但也会带来成本并产生新的工作量。综合来看，这是否真的带来了显著收益？Darbari表示："我越来越注意到，芯片设计公司——甚至是那些正在构建驱动智能体的AI硬件的公司——开始对初级工程师以及那些缺乏实际经验却自称专家的人过度使用智能体AI感到担忧。在前端它是高效的，但如果团队不够谨慎，在后端可能反而低效。"
这一状况可能随时间改善。Normal的Kao表示："这取决于规格说明的规模。从更宏观的角度看，如果我们将效率定义为节省工程师时间，那么考虑到验证智能体输出这项新任务，目前实际节省了多少工程时间还不明朗。随着模型持续改进以及我们找到更好的方式来验证智能体工作成果，效率提升空间值得期待。"
这一问题可以从多个维度衡量。Normal解决方案架构主管Arvind Srinivasan表示："复杂性的扩展不仅仅是计算层面的问题，还涉及数据完整性和审查方面的人工效率。与手写属性一样，规格说明中简单且文档完善的部分比设计中更复杂的部分更容易覆盖。为了实现现代设计中形式化覆盖的次线性扩展，需要将现有形式化工具与AI原生形式化工具以及非SVA的自动形式化策略相结合。"
规模扩展在使用形式化求解器时历来是重要议题。Aneja表示："形式化领域有许多有助于扩展的技术。好消息是，过去我们必须培训初级工程师掌握这些技术，而现在可以将这些知识内置于智能体中。当智能体编写属性时，可以非常高效地生成形式化属性，给出更好、更快的答案，让你在相同时间内完成更多工作，从而提升可扩展性。"
人在环路中
所有智能体流程目前都需要人类介入。Darbari表示："起草数百个候选属性过去需要数天的人工阅读，现在只需数分钟，这是真实的生产力提升。但效率可能消失的地方在于审查环节。如果每一个生成的属性或调试波形都需要与手动生成的一样深度的审查，而数量又增加了十倍，那么审查负担可能会超过起草阶段节省的时间。"
有人必须负责审查。Aneja表示："你不能直接拿来就用，否则会搬起石头砸自己的脚。大语言模型能做很多有趣的事情，但也能误导你，这是现实。它可以带来大量自动化，提升效率和生产力，但了解该设计的人必须手动审查、调整、引导，并不断积累这些经验。随着时间推移，也许可以对其进行训练，使其开箱即用就能做到相当合理的程度。"
大语言模型误导人的方式有很多。Darbari表示："空洞性检查、覆盖率分析以及与规格说明的交叉验证仍然必须进行，这些步骤不会因为生成速度加快而变得更快。团队应将空洞性检查和覆盖率检查作为标准实践，而非事后补充，因为生成的属性集比精心手写的属性集更容易包含平凡真命题。"
但这仍然带来了一个问题。Mao表示："人们希望保持控制权，因为他们要为后果负责。期望所有人都理解形式化方法似乎不太现实。那么，还有哪些其他表达形式可以用来验证规格说明的形式化表示是否准确？是波形吗？还是其他什么？"
标准实践需要内嵌到流程中。Darbari建议："将AI生成的属性视为草稿，而非已接受的可交付成果。在任何内容进入回归测试套件之前，在流程中设置一个审查关卡。用户应坚持要求可追溯性——每个属性对应哪个规格说明章节、哪项需求或哪个RTL构造——以便审查人员能够回溯并核查映射关系。"
随着信任的建立，收益会持续增长。Normal的Ilani表示："这对于希望进入形式化验证或基于断言的仿真领域的DV工程师来说是个好消息。多年来，我们常开玩笑说，编写有效的形式化属性需要博士学位。如今，AI驱动的流程降低了DV工程师进入形式化验证的门槛。在我看来，新方法论的一部分，就是充分利用智能体流程，让其成为你的得力助手——你的形式化验证博士助理——不仅帮助你理解形式化测试平台，还能运行它、调试失败案例并提出解决方案。"
参考文献
1. RAG-SVA in the Landscape of LLM-Based Assertion Generation，Cohen和Chibani
Q&A
Q1：知识图谱在AI生成SVA属性中起什么作用？
A：知识图谱将规格说明中的信息以"实体-关系"网络形式存储，包括节点（信号、模块、端口等）、边（驱动、复位、响应等关系）和三元组。相比普通RAG检索文本片段，知识图谱直接检索具体事实及其关联，减少大语言模型在生成属性时编造信号名称或误读关系的概率，从而提升生成属性的准确性和可靠性。
Q2：AI生成的形式化属性最大的风险是什么？
A：最大的风险是"虚假信心"。AI生成的SVA属性可能在语法上完全正确，但逻辑上过于宽松，或前置条件缺失、检查了错误的信号关系，导致形式化工具显示"通过"，实际上什么有意义的内容都没有被检查。此外，AI可能将自身对规格说明的错误解读固化为"事实"，一旦这些属性进入安全认证流程（如ISO 26262），影响将不局限于单一项目。
Q3：引入AI生成属性后，人工审查的工作量会减少吗？
A：不一定会减少。AI能在数分钟内生成过去需要数天才能完成的大量候选属性，但每个生成的属性仍需经过与手写属性同等深度的审查，包括空洞性检查、覆盖率分析和与规格说明的交叉验证。当生成数量增加十倍时，审查负担可能反而超过起草阶段节省的时间，整体投资回报率仍有待观察。
