LLM从技术规格到形式化属性

大语言模型（LLM）能否将一份技术规格文档，自动转换成一组形式化属性，用于对设计实现开展形式化验证？答案正在趋向肯定，但仍存在诸多限制条件。

核心要点

1. 大语言模型具备把规格文档转化为属性集合的能力。但绝大多数规格文档本身并不完善，AI 工具尚不成熟，整个过程仍需要大量人工介入。

2. 盲目采信 AI 工具输出结果存在隐患，必须借助其他手段来评估属性集合的完备性。

3. 投资回报尚不明确。虽然 AI 可以生成更多属性，但人工核验这些属性的成本会显著上升。

形式化验证长期面临的一大痛点，就是编写形式化属性门槛很高。尽管对应的语言标准已经问世二十余年，工具能力也得到巨大提升，但这道障碍始终未能彻底消除 —— 而现在，AI 或许正在改变这一局面。

大语言模型擅长阅读自然语言文档，并从中提炼整合信息。一个极具实用价值的应用方向便是读取设计规格，自动生成一套形式化属性，用来验证硬件实现是否与规格保持一致。

但该方向存在多项技术挑战，如果不能充分认识其中风险，很容易落入各类技术陷阱。

SystemVerilog 语言提供专门语法，可对设计属性做形式化定义。当这些属性被部署在验证环境中，就被称为断言（assertions）。属性用于定义信号之间的逻辑关系与时序关系，能够显式描述协议等行为。一套完整属性集合应当可以完整覆盖设计预期全部行为，并且不依赖于这些行为的具体实现方式。从这个角度来看，属性本身就构成一份评判 RTL 实现是否正确的参考规格。

但 SystemVerilog 断言（SVA）语言学习门槛很高。它属于声明式语言，和设计验证流程中多数编程语言所采用的面向对象、过程式编程范式截然不同。多年以来，行业一直在开发工具与方法论，降低属性编写难度。近期，基于大模型的工具取得明显进展，但仍有多项关键技术有待突破。

知识图谱是近期取得的一项技术突破，Cohen 与 Chibani 给出了相关定义：“知识图谱不以纯文本形式存储信息，而是以实体与实体之间关系的网络来保存数据。它由三部分构成：节点（实体，例如信号、模块、需求、端口）；边（实体关系，例如驱动、复位、响应、从属）；三元组作为基础存储单元，格式为（主体 → 关系 → 客体）。”

知识图谱相当于高速查询信息数据库，不需要大模型每次都重新抽取信息。“传统检索增强生成（RAG）返回的是看起来相关的文本片段；知识图谱返回确切事实以及事实之间的关联。这也是基于知识图谱框架可以获得更可靠事实依据的原因，模型编造信号名、误判实体关系的概率更低，因为关系已经被显式存储。”

颇具讽刺意味的一大现实难题，是很难拿到一份质量合格的规格文档。新思科技应用工程总监 Ravindra Aneja 表示：“理想状态是拥有一份完美规格，但过去至少三十年间，完美规格几乎不存在。绝大多数项目拿不到完善的规格，甚至有的项目完全没有规格文档。这取决于项目是全新开发还是衍生迭代、文档编写人员以及所属组织。在 AI 兴起之前，行业并不把完善规格文档当作优先事项。工程师经常在规格尚未定稿时就启动设计，因为脑海里已经有实现思路。AI 出现之后，规格文档才重新得到更多重视。”

现阶段 AI 已经可以完成不少工作。Axiomise 公司 CEO Ashish Darbari 谈到：“AI 可以读取规格文档、协议标准，甚至 RTL 代码注释，生成首轮断言，覆盖复位、握手、独热码状态以及基础安全检查。当规格来自稳定、少变更的标准协议时效果最好。AI 生成初稿，可以把编写模板化 SVA 断言这类枯燥工作自动化。”

业界很早就产生过这一技术诉求。西门子明导高级副总裁兼总经理 Abhi Kolpekwa 表示：“人们认为读取规格并转换为可使用的验证产物，非常适合由 AI 来完成。但同时还需要变更管理能力，因为规格文档本身会持续迭代。想要在验证流程中实现变更管理，仅靠 AI 智能体远远不够，这就需要上下文智能。我们需要构建上下文与上下文智能，不仅能够识别变更，还可以结合历史信息与潜在演进方向，在验证流程上下文内做出更合理的判断。”

规格文档从来都不是一成不变。新思科技 Aneja 讲道：“一边开发一边完善规格，市场部门又会提出新增功能需求，于是规格就要回退修改。变更幅度可大可小。无论规格如何改动，都需要搞清楚它会对设计本身、验证环境带来哪些影响。AI 很擅长识别改动点，分析改动会如何影响验证工作。行业内正在大量讨论如何管理这种伴随变更的设计流程，这正是 AI 可以发挥巨大价值的地方。”

潜在风险：陷阱重重

规格本身是否完备？Axiomise 的 Darbari 指出：“完备性是完全另一个层面的问题。现实芯片开发很少孤立开展。就算是全新项目，一份完整规格，完整覆盖架构、微架构以及接口（绝大多数 bug 都出现在接口），这种情况十分罕见。根据我的经验，AI 生成的属性集合，在结构、语法覆盖层面表现不错，但很难抓住架构意图，以及规则背后‘为什么要这么设计’。AI 输出具备实用价值，但完备性必须独立核验，需要充分理解设计意图的工程师去判断哪些行为被遗漏。”

全部关键信息是否被充分利用？Normal Computing 设计验证解决方案工程师 Yaron Ilani 表示：“断言的可用性与完备度，取决于 AI 引擎能力，以及 AI 对规格文档细微语义的理解精度。Normal Computing 的解决思路是执行自动形式化，生成本体模型。主要风险来自规格文档存在信息缺口、语义模糊，进而让 AI 产生错误假设。可以预先开展规格审计，缓解这类风险。”

以上两类问题，都会造成生成的属性集合不完备。 Darbari 警告：“最大的危险是虚假的安全感。团队拿到大批量 AI 生成属性，跑在形式化工具上看到全部证明通过，就直接拿来做签核。但形式化证明结果的可靠性完全取决于属性本身；薄弱或者空洞的属性会无意义地通过证明，实际上没有完成有效检查。AI 生成属性尤其容易出现该问题：语法合法的 SVA，但逻辑约束过于宽松、前件条件缺失或者约束过强，或是校验了错误的信号关系，代码依旧可以编译、形式证明直接通过。”

核验 AI 输出本身，就成为一项繁重验证任务。Normal 产品负责人 Hanna Yip 谈到：“从规格提取属性，本质是把非结构化、多模态信息提炼成可被证明的逻辑语句。信息抽取环节效率可以很高，但要保证抽取结果完全正确，难度很大。”

传统验证流程中，设计团队解读规格，验证团队解读规格，两组解读结果互相比对，有时还会发现规格文档自身就存在错误。Darbari 说道：“AI 生成属性，会悄无声息把自身对规格的错误理解固化，当作客观事实。解读错误被封装成看起来严谨的验证产物。还存在规模化风险：如果这些属性向下游供给 FMEDA 分析、安全案例，或是用于 ISO 26262、ISO 21434 认证材料，一处未被发现的漏洞，影响就不再局限于单一项目。”

这也意味着不能无条件信任 AI 产出。Normal 产品设计负责人 Kaye Mao 表示：“信任是一大难题。如何核验一份并非出自你手的工作产物？尤其 AI 智能体往往高度自信，输出结果表面看起来很合理。举个例子，如何确认生成的测试用例确实在按照规格校验设计？难道要全部去看波形吗？成本很高，因此需要创新手段来审核 AI 智能体输出。”

结合过往 AI 输出失控案例，Mao 提出另一项隐患：“另一个风险是没有限定 AI 智能体可访问的相关资料。只要有机会，AI 就会‘走捷径’。例如直接读取设计代码生成测试用例，这就违背了验证与设计相互独立的基本原则。”

投资回报（ROI）

尽管 AI 确实可以完成部分工作，但同时会带来额外工作量与成本。综合来看能否实现显著收益？

Darbari 表示：“我越来越多地看到芯片设计公司，哪怕是自研 AI 加速硬件的企业，都开始警惕初级工程师滥用智能体 AI，有些人没有实操经验，却宣称自己掌握全套技术。AI 在前期起草阶段效率很高，但如果团队把控不当，后期核查调试阶段会消耗大量人力。”

未来该状况可能改善。Normal 的 Kao 谈到：“要看规格文档规模大小。更深一层来看，如果将效率定义为节省工程师工时，那现在还很难下定论，因为新增了核验 AI 输出的任务。我相信随着模型能力迭代，以及核验 AI 产出的新手段出现，实际效率会逐步提升。”

评估维度是多方面的。Normal 解决方案架构负责人 Arvind Srinivasan 指出：“复杂度的缩放不能只看算力，还涉及人工审核、信息完备度带来的人力开销。和手写属性一样，规格中简单、文档完善的部分更容易被覆盖，复杂高级的设计逻辑则很难处理。想要现代设计下形式化覆盖实现次线性增长，需要在现有形式化工具基础上，补充面向 AI 原生的形式化工具，以及 SVA 以外的自动形式化方案。”

可扩展性一直是形式化求解器的关键指标。新思科技 Aneja 说道：“形式化领域已经存在大量提升规模的技术手段。过去我们需要培训初级工程师掌握这些技巧；现在可以把知识库内置到 AI 智能体中。AI 在编写形式化属性时就可以善用这些技术，输出质量更好、求解速度更快，同等时间内完成更多工作，改善整体可扩展性。”

人在回路（Human‑in‑the‑loop）

现阶段所有 AI 智能体工作流，都必须保留人的介入。

Darbari：“过去需要数天人工阅读整理，现在几分钟就可以生成数百条候选属性，这是实实在在的生产力提升。但效率损耗会出现在审核环节。如果每一条 AI 生成属性、每一段调试波形，都要和手写产物同等深度审查，而数量翻十倍，审核负担就会抵消起草环节节省的时间。”

必须安排人员做审核。Aneja：“不能直接拿来就用，否则只会带来麻烦。大模型能完成很多有价值工作，但同样会误导人，这就是现实。AI 可以带来自动化，提升效率，但熟悉设计的工程师必须人工复核、修改、引导模型，不断沉淀知识。长期来看，可以持续训练模型，最终实现开箱可用的不错效果。”

大模型的误导形式多种多样。Darbari：“空洞性检查、覆盖率分析、对照规格交叉校验必不可少，不会因为生成速度变快而变得简单。应当将空洞检查、覆盖率检查设为标准强制步骤，而不是事后补救。AI 生成属性集合相比手工编写，更容易出现空洞恒真属性。”

这里还引出管理层面矛盾。Mao 表示：“工程师希望保持掌控，毕竟要为最终结果负责。要求所有人精通形式化并不现实。那我们还可以用什么表达形式，去核验规格对应的形式化描述是否准确？波形？还是其他手段？”

必须把规范流程固化进开发流程。Darbari 给出建议：“把 AI 生成属性当作草稿，绝对不要当作正式交付产物。在进入回归测试套件之前设置审核关卡。要求保留溯源信息，每一条属性要记录来自规格哪一节、哪条需求，或是哪一段 RTL 代码，方便审核人员回溯核对映射关系。”

建立可信工作流之后，收益会进一步放大。Normal 的 Ilani 谈到：“这对于希望入门形式化验证、断言仿真的 DV 工程师是利好。过去行业有句玩笑：写出高质量形式化属性需要博士水平。AI 驱动的工作流降低形式化验证的入门门槛。我认为新方法论应当善用 AI 智能体，把它当作你的助手，相当于拥有一位形式化验证助理博士，协助你搭建、运行形式化测试平台，定位失败原因，给出修复思路。”