Knowledge Graph: The Overlooked Key Link in Agentic AI Formal Verification

This paper proposes a knowledge graph-based formal verification method that connects specifications, RTL designs, and tool feedback via structured intermediate representations. It constructs a multi-agent workflow to achieve three optimizations: syntax repair, counterexample guidance, and coverage enhancement, achieving a formal coverage rate of 78.5% to 99.4% across seven benchmark designs. This method bridges the semantic gap of text-only approaches and provides critical infrastructure for agentic AI-driven formal verification.

Formal verification is the gold standard for ensuring the correctness of hardware designs, but the bottleneck of assertion writing limits its application. While LLMs bring hope for automatic SVA generation, they face three major challenges: specification ambiguity, RTL detail criticality, and semantic mismatch. Current mainstream methods treat specifications and RTL as loose text, leading to parsing failures, semantic mismatches, and difficulty in using tool feedback for iteration.

The verification-centric knowledge graph integrates information from three sources: 1. Specification IR (functional requirements, timing constraints, etc.); 2. RTL IR (module hierarchy, signal definitions, etc.); 3. Formal tool feedback (syntax diagnosis, counterexamples, coverage reports). Its core values include: traceable specification anchoring, design-aware context retrieval, and semanticization of tool feedback.

The knowledge graph-based multi-agent workflow includes four roles: Query Agent (converts natural language to KG queries), Generation Agent (generates candidate SVA), Verification Agent (submits to tools and collects feedback), and Repair Agent (diagnoses and fixes issues). Three refinement loops: 1. Syntax repair (uses KG information to correct syntax errors); 2. Counterexample-guided correction (maps counterexamples to requirements via trace links); 3. Coverage enhancement (associates coverage gaps with requirements to generate new assertions).

The experiment was evaluated on seven benchmark designs: In terms of syntax correctness, the generated SVA has a high compilation pass rate and low repair overhead; formal coverage reaches 78.5% to 99.4%, which is on average higher than the text-only baseline; convergence shows design dependency—control logic designs perform well, while complex timing and arithmetic reasoning designs are still limited by LLM capabilities.

Adopting the knowledge graph method requires attention to: upfront investment (toolchain setup, IR extractor development, etc.); integration with existing processes (API design and automation scripts to reduce costs); incremental update mechanism; interpretability requirements (important in safety-critical domains); LLM selection (general-purpose or domain-specific models).

Current limitations: Difficulty in complex timing reasoning, arithmetic reasoning challenges, KG scale and query efficiency bottlenecks for ultra-large-scale designs, dynamic update requirements. Future directions: Combining symbolic and neural reasoning, applying GNN to KG reasoning, domain-specific LLMs, extending to other verification tasks such as simulation test generation.

The knowledge graph method significantly improves the quality and efficiency of assertion generation by explicitly modeling the relationships between specifications, designs, and tool feedback. Despite its limitations, it opens a new path for formal verification automation. As LLM and KG technologies mature, fully automated formal verification of complex chip designs is expected to be achieved.