大型语言模型正逐步执行芯片设计验证中最令人困扰的任务之一：将自然语言撰写的规格转换为一组可用于判断 RTL 实现正确性的形式化属性。Semiconductor Engineering 的 Brian Bailey 进行的采访表明，当前工具能够生成有用的初始草稿，但距离在没有大量工程审查的情况下创建一套完整、可采纳的属性集仍相去甚远。
这一进展之所以重要，是因为多年来属性编写一直是形式化验证的瓶颈。SystemVerilog 属性在验证环境中被称为 assertions，用于描述信号之间的逻辑和时序关系，例如复位行为、握手、one-hot 条件以及基本安全检查。当这些属性完整且准确时，便可用于将 RTL 实现的行为与规格进行比较，而不受设计构建方式的影响。
当前工具能做什么？
基于大型语言模型的工具可以读取规格文档、协议标准，甚至 RTL 内的注释，然后提出 SVA 属性草稿。Axiomise 首席执行官 Ashish Darbari 表示，当规格基于变化不大的稳定标准时，这种应用更具可行性。在这种情况下，工具可以减轻初始代码编写中重复性的部分，而不是接管整个验证过程。
一些方法正尝试通过创建 knowledge graph（即存储实体及其关系的知识图谱）来提高模型的准确性。节点可能包括信号、模块、需求或端口，而边则描述“驱动”“复位”和“响应于”等关系。系统不再检索看似与请求相关的文本片段，而是可以回溯到明确的事实和联系，从而降低虚构信号名称或误解设计组件之间关系的可能性。消息来源在这一语境下提到了 Cohen 和 Chibani 的论文 RAG-SVA in the Landscape of LLM-Based Assertion Generation。
问题在人工智能之前就已开始
工具无法提取原本没有被写下或确定的内容。Synopsys 应用工程总监 Ravindra Aneja 表示，过去三十年中，理想的规格从来都不是唾手可得的；开发往往在文档完成之前就已开始，而在某些项目中可能根本不存在完整规格，尤其是在衍生设计中，或需求在工作过程中发生变化时。
这个问题不只是措辞问题，还涉及变更管理。营销团队可能会增加新功能或修改现有需求，设计和验证团队则必须确定该变更的影响。Siemens EDA 高级副总裁兼总经理 Abhi Kolpekwa 认为，将规格转换为属性需要能够跟踪变更历史及其背景的“上下文智能”，而不是一个每次都生成新文本的代理。
虚假信任的风险
当前方法最大的限制是，某个属性可能在语法上正确，因而能够被编译，验证工具也能证明它成立，但它并没有真正测试预期行为。Darbari 警告称，薄弱或 vacuous 的属性可能很容易通过，因为它允许大量行为，或者使用了错误的信号，又或者缺少前置条件或施加了过度限制。因此，“绿色证明”并不意味着设计没有错误；证明的强度不会超过被证明属性本身的强度。
消息来源还指出，与理解架构意图及规则存在的原因相比，模型在结构和语法覆盖方面往往表现更好。因此，模型对规格的不准确解读可能会转化为一段看似正式且严谨的内容，同时掩盖需求缺口。如果这一缺口延伸到 FMEDA、功能安全文件或与 ISO 26262 和 ISO 21434 相关的认证证据中，其影响可能超出原始验证项目本身。
设计与验证的分离同样是一个突出问题。Normal Computing 产品设计负责人 Kaye Mao 指出，有必要限制代理能够访问哪些项目材料，因为允许代理使用设计本身来生成测试用例，可能会削弱验证过程的独立性。
实际会发生什么变化？
据 Darbari 称，人工智能可以将初始草稿的准备时间从几天缩短到几分钟，但也可能使后续工作量增加一倍。每个生成的属性都需要根据规格进行检查、进行覆盖率分析、执行 vacuity 测试，并审查其与设计信号的关系；失败项可能还需要进行波形分析。如果属性数量增加十倍，而每个属性所需的审查程度保持不变，那么审查负担可能超过快速生成所带来的收益。
从 certi.news 的角度看，真正的变化不是取代验证工程师，而是将重心从编写属性转向评估属性及追踪其来源。Darbari 建议将生成的属性视为草稿，而不是经批准的输出，并在将其纳入 regression suite 之前设置审查关卡。同时还应记录每个属性的来源：生成它的规格段落、需求或 RTL 元素，以便工程师核实其一致性。
Normal Computing 验证解决方案工程师 Yaron Ilani 表示，这种方法可以降低希望使用 formal verification 的验证工程师的入门门槛。但这并不能解决投资回报问题。Kaye Mao 认为，验证代理输出所需的时间必须计入成本；而 Normal Computing 首席解决方案工程师 Arvind Srinivasan 指出，扩展并不只与计算能力有关，还取决于数据的完整性和人工审查成本。
总而言之，大型语言模型已经能够加速属性编写中自动化且重复的部分，但尚未解决规格完整性和理解设计意图这两个问题。这些工具的价值仍将取决于是否有理解设计的工程师，以及用于衡量覆盖率、发现空属性或不合适属性的独立机制，而不是取决于模型能够生成多少属性。