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

TL;DR

ProofLoop is a novel tool that automates the generation of SystemVerilog Assertions from natural language by combining language models with formal verification tools in a two-phase, iterative process.

Contribution

It introduces a solver-in-the-loop approach with retrieval-augmented generation and formal proof feedback, improving correctness in SVA generation from natural language.

Findings

Achieves 93.7% syntax correctness in SVA generation.

Achieves 82.0% functional correctness in verification.

Each component (retrieval, formal tools, verification loop) significantly improves performance.

Abstract

SystemVerilog Assertions (SVA) are essential for formal verification of digital hardware, yet their manual creation demands significant expertise in both the design under verification and temporal logic. Recent studies have explored using large language models (LLMs) to automate SVA generation, but existing approaches suffer from incorrect signal references, missing timing constraints, and lack of formal correctness guarantees. This paper presents ProofLoop, a tool-augmented ReAct agent that generates SVA from natural-language specifications using a solver-in-the-loop approach. The agent operates in two phases: Phase A autonomously gathers design context by invoking EDA and formal tools, including semantic search over an AST-indexed vector database and JasperGold structural queries, while Phase B generates SVA and iteratively refines it using JasperGold formal proof feedback over up to fixed (here 3) verification rounds. We evaluate ProofLoop on FVEval Design2SVA design benchmarks and demonstrate that this framework can achieve 93.7% syntax correctness and 82.0% functional correctness. An ablation study confirms that each component, i.e., retrieval-augmented generation (RAG), JasperGold tools, and the verification loop contributes significantly (and orthogonally).