From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation

Technical Summary: ProofLoop: Bridging LLMs & Formal Representations for RTL Assertion Generation

1. Problem Statement

The verification of modern digital hardware relies heavily on Assertion-Based Verification (ABV) using SystemVerilog Assertions (SVA). However, authoring high-quality SVA is a bottleneck in the design cycle because it requires deep expertise in both Register-Transfer Level (RTL) semantics and temporal logic.

While Large Language Models (LLMs) have been applied to automate SVA generation, existing methods face three critical failures:

• Lack of Structural Awareness: LLMs cannot "see" hardware metadata (e.g., clock domains, reset behaviors, signal fan-in/fan-out) from raw text, leading to incorrect signal references.
• Temporal Mismatches: LLMs often struggle to align natural language intent with the actual timing/sequential behavior of the hardware.
• Lack of Formal Guarantees: Standard prompting lacks a feedback mechanism to correct syntax errors or logical inconsistencies identified by formal tools.

2. Methodology: The ProofLoop Framework

The authors propose ProofLoop, a tool-augmented ReAct (Reasoning + Acting) agent that utilizes a solver-in-the-loop approach. The framework operates in three distinct stages:

• Stage 1: AST-Based Knowledge Base Construction: Instead of feeding raw RTL into the LLM, the system parses the SystemVerilog code into an Abstract Syntax Tree (AST). The AST is decomposed into semantic chunks (Module Interfaces, Always Blocks, Instances, and Assignments) and stored in a vector database for Retrieval-Augmented Generation (RAG).
• Stage 2: Phase A (Agentic Context Gathering): A ReAct agent enters a reasoning loop (up to 6 rounds) to autonomously decide which tools to invoke. It uses two types of tools:
  • Retrieval Tools: Perform semantic searches over the AST-indexed database to find relevant code fragments.
  • Structural Analysis Tools: Interface with Cadence JasperGold to extract hardware-level metadata (e.g., signal dependencies and flip-flop properties) that are not explicitly clear in the text.
• Stage 3: Phase B (Iterative Verification Loop): The agent generates SVA and submits it to JasperGold. If the assertion is falsified or contains syntax errors, the solver’s error messages and counterexample traces are fed back to the agent. The agent then performs targeted repairs (up to 3 rounds) rather than regenerating the code from scratch.

3. Key Contributions

1. Agentic Context Synthesis: Moving beyond static RAG by allowing an agent to dynamically query structural and semantic information.
2. Solver-in-the-Loop Refinement: Integrating formal verification feedback directly into the LLM's reasoning cycle to enable surgical error correction.
3. Scalable Architecture: A modular approach that handles complex, multi-module designs by managing context through AST-based retrieval rather than massive, monolithic prompts.

4. Experimental Results

The framework was evaluated using the FVEval Design2SVA benchmark on NVIDIA H100 GPUs, comparing the "Pipeline" approach against a "Baseline" (direct prompting).

• Performance Gains: Using Qwen3.5-35B, the pipeline achieved 93.7% syntax correctness and 82.0% functional correctness, nearly doubling the functionality of the baseline (43.2%).
• Complexity Scaling: The advantage of ProofLoop grows with design complexity. While the baseline performs reasonably on single-module designs, its performance degrades on large, multi-module designs where the context exceeds the LLM's window. ProofLoop remains stable due to its retrieval mechanism.
• Ablation Study: The study confirmed that the Verification Loop and Structural Analysis Tools provide the most significant contributions, followed by RAG.
• Benchmark Superiority: On the Design2SVA task, ProofLoop (Qwen3.5-35B) significantly outperformed state-of-the-art models like GPT-4o and Gemini-1.5-Pro in both Pass@1 and Pass@5 metrics.

5. Significance

This research represents a shift from treating LLMs as mere "code writers" to treating them as intelligent verification agents. By bridging the gap between high-level natural language and low-level formal logic through tool augmentation, ProofLoop demonstrates a viable path toward automating the most labor-intensive aspects of hardware verification. This approach is particularly significant for the industry as SoC (System-on-Chip) complexity continues to outpace manual verification capabilities.