Knowledge Graphs, the Missing Link in Agentic AI-ba...

Knowledge Graphs, the Missing Link in Agentic AI-ba... | AI Research

Key Takeaways

Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification Formal Verification (FV) is a critical process in hardware design that ensures a s...
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).
The KG links requirements, design hierarchy, signals, assumptions, and properties to provide traceable, design-grounded context for generation.
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.

Paper AbstractExpand

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.

Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification
Formal Verification (FV) is a critical process in hardware design that ensures a system behaves correctly under all possible conditions. While Large Language Models (LLMs) have shown promise in automating the creation of SystemVerilog Assertions (SVAs)—the building blocks of formal verification—they often struggle with ambiguous specifications and complex hardware details. This paper introduces a verification-centric Knowledge Graph (KG) approach that links design requirements, RTL code, and formal tool feedback into a structured, queryable format. By using this graph as a "source of truth," a multi-agent system can generate more accurate assertions and perform iterative refinements to fix errors and improve coverage.

Bridging the Gap Between Specs and Code

A major challenge in AI-assisted verification is the "grounding" problem: LLMs often treat specifications and hardware code as disconnected text, leading to syntax errors and semantic mismatches. This research addresses this by extracting structured Intermediate Representations (IRs) from the design. These IRs act as a bridge, mapping natural-language requirements to specific hardware signals and module hierarchies. By organizing this data into a Knowledge Graph, the system provides the AI with a clear, traceable context, ensuring that the generated assertions are grounded in the actual design implementation rather than just general language patterns.

Multi-Agent Refinement Loops

The methodology employs a team of specialized AI agents that work together to manage the verification lifecycle. Instead of relying on a single prompt, the system uses agents for specific tasks: interpreting requirements, grounding signals, synthesizing temporal logic, and debugging. The system drives three distinct refinement loops:

Syntax Repair: Uses tool diagnostics to automatically fix compilation errors.
CEX-Guided Correction: Uses Counterexamples (CEXs) from the formal tool to trace failures and adjust assertions.
Coverage-Directed Augmentation: Analyzes coverage reports to identify gaps and generate new properties to verify previously untested logic.

Performance and Results

The approach was evaluated across seven benchmark designs, including FIFOs, ALUs, and Binary Search Trees. The results demonstrate that the Knowledge Graph-based context retrieval consistently produces compilable SVAs with minimal manual intervention. The system achieved formal coverage ranging from 78.5% to 99.4%. The use of the KG significantly reduced common front-end issues like incorrect signal references or macro mismatches, making the verification workflow more reliable and repeatable.

Current Limitations

While the system is highly effective at generating and fixing standard assertions, the authors note that complex designs remain challenging. Specifically, properties requiring deep temporal reasoning, global data-structure invariants, or complex arithmetic logic still exceed the current capabilities of LLMs. Additionally, the convergence of the refinement loops is design-dependent; while some designs see significant improvements through automated patching, others require more sophisticated, inductive reasoning strategies that are currently beyond the scope of local, agent-based correction.