Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification

Technical Summary: Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification

Problem Statement
While Large Language Models (LLMs) have demonstrated potential in generating SystemVerilog Assertions (SVAs) from natural-language specifications to accelerate Formal Verification (FV), significant hurdles remain. The primary challenge is the "grounding" problem: specifications are often ambiguous or incomplete, while critical micro-architectural details reside in the Register Transfer Level (RTL) code. Existing approaches typically treat specifications and RTL as loosely structured text, leading to weak specification-to-RTL grounding. This results in semantic mismatches, frequent syntax failures during formal parsing, and assertions that require extensive iterative correction and manual triage. Furthermore, prior methods often fail to persistently integrate formal-tool feedback (such as Counterexamples or CEXs and coverage reports) into the generation loop, limiting systematic refinement.

Methodology
The authors propose a verification-centric methodology that constructs a Knowledge Graph (KG) from structured Intermediate Representations (IRs) to bridge the gap between intent and implementation. The workflow is organized into four layers: Inputs, Typed JSON IRs, Runtime KGs, and Agent Orchestration.

1. Intermediate Representations (IRs): The system extracts and normalizes data into typed JSON artifacts, including spec_chunks.json (hierarchical specifications), requirements.json, design_model.json (RTL metadata like hierarchies and signals), properties.json, and verification outcomes (formal_results.json, cex_cases.json, coverage_metrics.json).
2. Knowledge Graph Construction: These IRs are exported as nodes and edges to build a runtime KG using NetworkX. The KG acts as an artifact registry, linking requirements, design hierarchy, signals, assumptions, and properties. It enables bounded context retrieval; for instance, when generating a property, the KG provides the specific requirement, its parent specification fragment, relevant RTL signals, and rulebooks.
3. Multi-Agent Orchestration: The verification process is decomposed into specialized agents that query and update the KG:
   • Property Generation: A lead agent coordinates a spec_analyst (decomposing requirements), sva_author (synthesizing SVA syntax), sva_reviewer (validating adherence), and sva_patcher (correcting based on feedback).
   • Syntax Correction: A dedicated loop handles compilation errors. Agents analyze diagnostics, apply deterministic repairs for common patterns (e.g., undeclared identifiers), and use complex context (RTL declarations, requirement text) for harder errors. Properties are allowed a maximum of three correction attempts.
   • CEX Correction: When properties fail, agents parse VCD waveforms and failure traces. A spec_assertion_analyzer classifies root causes (e.g., RTL bugs vs. under-specification), and a cex_fixer adjusts constraints or strengthens assertions.
   • Coverage Improvement: Agents analyze coverage metrics to identify unreachable code or vacuous properties, generating targeted properties to close gaps.

Key Contributions
The paper claims three primary contributions:

1. Verification-Centric KG Construction: A novel approach building a KG from structured IRs that integrates specification intent, RTL structure, generated properties, and formal-tool results into a single, queryable artifact.
2. Multi-Agent Workflow with Traceability: A system where agents use KG-grounded context to generate and refine SVAs, maintaining explicit trace links from requirements to design elements, properties, and verification outcomes.
3. Empirical Evaluation: An assessment on seven open-source benchmark designs quantifying the impact of KG-grounded context on property generation effectiveness, syntactic validity, and the efficacy of CEX refinement loops.

Results
The methodology was evaluated on seven designs (FIFO, Lemming, ALU, CICD, BST, TTC Counter, and CSR) using the GPT-5.2 model and Cadence JasperGold.

• Syntax and Compilation: The approach consistently produced compilable SVAs with low syntax-repair overhead. The KG-grounded context, particularly the deterministic resolution of signals and hierarchy via the design_model IR, significantly reduced front-end issues like undeclared identifiers.
• Formal Coverage: End-to-end formal coverage ranged from 78.5% to 99.4% across the benchmarks.
• Refinement Efficacy: Designs like FIFO and CIC Decimator showed significant improvement after CEX and coverage loops, suggesting many initial failures were due to local issues (missing guards, boundary conditions) correctable via retrieved context.
• Limitations: Convergence was design-dependent. Complex designs like the Binary Search Tree (BST) and those requiring global invariants or deep temporal reasoning (e.g., Lemming, ALU) showed limited improvement from automated correction. The authors note that current LLM capabilities struggle with complex temporal and arithmetic reasoning, and semantic debugging remains the primary bottleneck for harder benchmarks.

Significance
The paper posits that the proposed KG-centric approach addresses the critical weakness of prior work: the lack of structured, queryable links between requirements, RTL semantics, and verification outcomes. By treating formal-tool feedback (CEXs, coverage gaps) as persistent, queryable KG content rather than transient outputs, the system enables a closed-loop refinement process. The authors conclude that while semantic correction for complex reasoning remains a challenge, this framework provides a robust foundation for traceable, design-grounded property generation. As LLM capabilities advance, they will be better positioned to leverage the structured context and traces provided by this KG, further improving the reliability of automated formal verification.