知识图谱：Agentic AI形式验证中被忽视的关键纽带

本文提出基于知识图谱的形式验证方法，通过结构化中间表示连接规格说明、RTL设计和工具反馈，构建多Agent工作流实现语法修复、反例引导和覆盖增强三重优化，在七个基准设计中实现78.5%-99.4%的形式覆盖率。该方法弥补了纯文本方法的语义鸿沟，为Agentic AI驱动的形式验证提供关键基础设施。

形式验证是确保硬件设计正确性的黄金标准，但断言编写瓶颈制约其应用。LLM虽带来自动生成SVA的希望，但面临三大挑战：规格说明模糊性、RTL细节关键性、语义不匹配。现有主流方法将规格和RTL视为松散文本，导致解析失败、语义不匹配及难以利用工具反馈迭代。

验证中心知识图谱整合三个来源信息：1.规格说明IR（功能需求、时序约束等）；2.RTL IR（模块层次、信号定义等）；3.形式工具反馈（语法诊断、反例、覆盖率报告）。其核心价值包括：可追溯的规格锚定、设计感知的上下文检索、工具反馈的语义化。

基于知识图谱的多Agent工作流包含四个角色：查询Agent（转换自然语言为KG查询）、生成Agent（生成候选SVA）、验证Agent（提交工具收集反馈）、修复Agent（诊断并修复问题）。三重精炼循环：1.语法修复（利用KG信息修正语法错误）；2.反例引导修正（通过trace links映射反例到需求）；3.覆盖增强（关联覆盖率缺口与需求生成新断言）。

实验在七个基准设计上评估：语法正确性方面，生成的SVA编译通过率高且修复开销低；形式覆盖率达78.5%-99.4%，平均高于纯文本基线；收敛表现出设计依赖性——控制逻辑设计效果好，复杂时序和算术推理设计仍受LLM能力限制。

采用知识图谱方法需关注：前期投入（工具链搭建、IR提取器开发等）；与现有流程集成（API设计和自动化脚本降低成本）；增量更新机制；可解释性需求（安全关键领域重要）；LLM选择（通用或专用模型）。

当前局限：复杂时序推理困难、算术推理挑战、超大规模设计的KG规模与查询效率瓶颈、动态更新需求。未来方向：结合符号与神经推理、GNN应用于KG推理、领域专用LLM、扩展到仿真测试生成等其他验证任务。

知识图谱方法通过显式建模规格、设计和工具反馈的关系，显著提升断言生成质量与效率。虽存在局限，但为形式验证自动化开辟新道路。随着LLM和KG技术成熟，有望实现复杂芯片设计的全自动形式验证。