Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification
作者: Vaisakh Naduvodi Viswambharan, Keerthan Kopparam Radhakrishna, Deepak Narayan Gadde, Aman Kumar
分类: cs.AI
发布日期: 2026-05-07
备注: To appear at the IEEE International Conference on IC Design and Technology 2026 (ICICDT), June 22 - 24, 2026, Dresden, Germany
💡 一句话要点
提出基于知识图谱的Agentic AI形式验证方法，提升SystemVerilog断言生成质量。
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 知识图谱 形式验证 SystemVerilog断言 Agentic AI RTL验证
📋 核心要点
- 现有方法在自然语言规范生成SystemVerilog断言时，缺乏规范到RTL的有效对齐，导致语义不匹配和语法错误。
- 构建验证为中心的知识图谱，连接需求、设计层次、信号等，为断言生成提供可追溯的设计上下文。
- 实验表明，该方法能生成可编译的SystemVerilog断言，形式覆盖率达到78.5%到99.4%，但复杂推理仍具挑战。
📝 摘要（中文）
本文提出了一种基于知识图谱（KG）的Agentic AI形式验证方法，旨在解决现有方法在从自然语言规范生成SystemVerilog断言（SVA）时面临的挑战。现有方法通常将规范和RTL视为松散结构的文本，导致规范到RTL的对齐不足，语义不匹配以及形式解析和精化期间频繁的语法失败。本文构建了一个以验证为中心的知识图谱，该图谱由从规范、RTL和形式工具反馈（包括语法诊断、反例（CEX）和覆盖率报告）中提取的结构化中间表示（IR）组成。该知识图谱连接需求、设计层次结构、信号、假设和属性，为生成提供可追溯的、基于设计的上下文。一个多Agent工作流程查询和更新该知识图谱以生成SVA，并驱动三个改进循环：工具诊断指导的语法修复、使用跟踪链接的CEX指导的校正以及覆盖率指导的属性增强。在七个基准设计上的评估表明，基于知识图谱的上下文检索提高了规范到RTL的对齐，并始终产生具有低语法修复开销的可编译SVA。该方法实现了78.5%到99.4%的形式覆盖率，但收敛性表现出设计依赖性，复杂的时序和算术推理对当前的LLM能力仍然具有挑战性。
🔬 方法详解
问题定义：现有方法在将自然语言规范转换为SystemVerilog断言（SVA）时，面临着规范和RTL之间缺乏有效关联的问题。规范通常是模糊或不完整的，而关键的微架构细节则存在于RTL中。现有方法将规范和RTL视为非结构化的文本，导致规范到RTL的映射不准确，从而产生语义不匹配和语法错误，最终影响形式验证的效率和准确性。
核心思路：本文的核心思路是构建一个以验证为中心的知识图谱（KG），该图谱能够捕获规范、RTL和形式验证工具反馈中的关键信息，并将它们以结构化的方式连接起来。通过知识图谱，可以为断言生成提供更丰富、更准确的上下文信息，从而提高SVA生成的质量和效率。这种设计旨在弥合自然语言规范和RTL实现之间的语义鸿沟。
技术框架：该方法采用一个多Agent工作流程，该流程的核心是知识图谱。整体流程包括以下几个阶段：1) 从规范、RTL和形式验证工具的反馈中提取结构化的中间表示（IR）；2) 构建知识图谱，将需求、设计层次结构、信号、假设和属性等信息连接起来；3) 使用多Agent系统查询和更新知识图谱，生成SVA；4) 通过三个改进循环来优化SVA：语法修复（由工具诊断指导）、CEX指导的校正（使用跟踪链接）和覆盖率指导的属性增强。
关键创新：该方法最重要的创新点在于利用知识图谱来显式地表示和管理验证过程中的各种信息。与现有方法相比，该方法能够更好地理解规范和RTL之间的关系，从而生成更准确、更可靠的SVA。此外，多Agent工作流程和改进循环能够有效地利用形式验证工具的反馈，从而提高SVA的质量和覆盖率。
关键设计：知识图谱的构建是关键。它需要定义合适的实体类型和关系类型，以便能够有效地表示规范、RTL和形式验证工具反馈中的信息。多Agent系统的设计也至关重要，需要定义每个Agent的角色和职责，以及它们之间的协作方式。此外，改进循环的设计也需要仔细考虑，需要选择合适的反馈指标和优化策略，以便能够有效地提高SVA的质量和覆盖率。具体的参数设置、损失函数和网络结构等细节未在摘要中详细描述，属于未知信息。
🖼️ 关键图片
📊 实验亮点
实验结果表明，基于知识图谱的上下文检索能够有效提高规范到RTL的对齐，并始终生成可编译的SystemVerilog断言，且语法修复开销较低。该方法在七个基准设计上实现了78.5%到99.4%的形式覆盖率。虽然收敛性存在设计依赖性，且复杂时序和算术推理仍面临挑战，但整体性能表现优于现有方法。
🎯 应用场景
该研究成果可应用于集成电路设计验证领域，特别是形式验证流程。通过提升SystemVerilog断言的生成质量和效率，可以显著缩短验证周期，降低验证成本，并提高芯片设计的可靠性。该方法有望推动形式验证技术的普及，并促进更复杂、更可靠的硬件系统的开发。
📄 摘要（原文）
Recent advances in Large Language Models (LLMs) have enabled workflows that generate SystemVerilog Assertions (SVAs) from natural-language specifications, with the potential to accelerate Formal Verification (FV). However, high-quality assertion synthesis remains challenging because specifications are often ambiguous or incomplete and critical micro-architectural details reside in the Register Transfer Level (RTL). Many existing approaches treat the specification and RTL as loosely structured text, which weakens specification-to-RTL grounding and leads to semantic mismatches and frequent syntax failures during formal parsing and elaboration. This work addresses these limitations with a verification-centric Knowledge Graph (KG) constructed from structured Intermediate Representations (IRs) extracted from the specification, RTL, and formal-tool feedback, including syntax diagnostics, Counterexamples (CEXs), and coverage reports. The KG links requirements, design hierarchy, signals, assumptions, and properties to provide traceable, design-grounded context for generation. A multi-agent workflow queries and updates this KG to generate SVAs and to drive three refinement loops: syntax repair guided by tool diagnostics, CEX-guided correction using trace links, and coverage-directed property augmentation. Evaluation across seven benchmark designs indicates that KG-based context retrieval improves specification-to-RTL grounding and consistently produces compilable SVAs with low syntax-repair overhead. The approach achieves formal coverage ranging from 78.5% to 99.4%, though convergence exhibits design dependence with complex temporal and arithmetic reasoning remaining challenging for current LLM capabilities.