PRO-V-R1: Reasoning Enhanced Programming Agent for RTL Verification

Motivation

• RTL verification depends on executable testbenches and consumes 60% to 70% of total development time, making it a significant hardware-design bottleneck.Testbenches stimulate the DUT, monitor responses, and compare outputs with expected behavior.Source: §1 · p. 1
• LLM research predominantly targets RTL generation, whose performance exceeds testbench generation, despite verification being critical and more challenging.Figure 1 contrasts RTL-generation and testbench-generation performance across LLMs.Source: §1 · p. 1, Figure 1 · p. 1
• Current verification approaches often use proprietary LLMs to generate Python functional reference models because these models are stronger at Python than Verilog.This approach is associated with high inference costs, data-privacy risks, and limited fine-tuning.Source: §1 · p. 1
• Python-based verification can suffer hallucinations when Python and Verilog indexing or slicing semantics diverge, while open-source verification datasets and training frameworks remain absent.Figure 2 illustrates differences in significance-based Verilog indexing and inclusive slicing versus Python conventions.Source: §1 · p. 2, Figure 2 · p. 2

Contributions

• The framework addresses agent inefficiency, scarce verification-specific SFT data, and the lack of an RL framework for optimizing autonomous verification workflows.These challenges arise from expensive agent execution, design-oriented public datasets, and missing dedicated training methods.Source: §1 · p. 2
• PRO-V-R1 combines the PRO-V sys agentic system, simulation-validated expert trajectories for SFT, and verification-specific RL rewards from programmatic tool feedback.The framework is presented as an end-to-end open-source solution for autonomous RTL verification.Source: §1 · p. 2

Results

• PRO-V-R1 achieves 57.7% functional correctness and 34.0% fault detection, outperforming SOTA agent-system baselines at 25.7% and 21.8%, respectively, with an 8.8× speedup.It averages 91 s/task.Source: §1 · p. 2

2.1 LLM-based Verilog generation and verification

• LLM-aided RTL verification increasingly generates Python functional reference models in agent-controllable environments instead of complete HDL testbenches.This shift reflects the difficulty of direct HDL generation and the relative strength of code LLMs on Python.Source: §2.1 · p. 2
• Proprietary-model dependence brings high inference costs, data-privacy risks, hallucinations across Python and Verilog semantics, and few open reproducible verification resources.The resulting scarcity covers specialized agent systems, curated datasets, and training frameworks.Source: §2.1 · p. 2

2.2 Tool-Enhanced LLM Agents with Post-training

• Tool-enhanced agents use LLM controllers with domain-specific tools, typically establishing policies through expert-demonstration SFT and refining them through RL from environmental feedback.A scalar verified reward favors actions that produce high-reward outcomes.Source: §2.2 · p. 2
• Hardware verification has not yet benefited fully from SFT-then-RL because it lacks verified reasoning traces, dense rewards from sparse simulation outcomes, and effective credit assignment for multi-step workflows.The paper presents its training loop as addressing these three domain-specific challenges.Source: §2.2 · p. 2

3 Methods

• The framework combines modular verification agents and programmatic tools with an agentic training framework for autonomous RTL verification.The system includes an agentic verification system and a training framework that optimizes the full workflow.Source: §3 · p. 2, §3.1 · pp. 2–3

3.1 Agentic Verification System

• Testcase Generation uses a Python Code Interpreter to construct bit-accurate, width-sensitive, coverage-driven input sequences instead of emitting long numerical vectors directly.This approach addresses LLM weaknesses in generating long numerical sequences and produces functionally valid stimuli.Source: §3.1 · p. 3
• FRM Generation combines JSON input signals with the RTL specification and sampled Python functional reference models to produce cycle-aligned expected outputs.Executable FRMs compute expected outputs for the generated testcases, applying precise logic to reduce direct arithmetic errors.Source: §3.1 · p. 3
• Iterative Refinement selects candidates by majority vote, verifies them, applies targeted testbench edits, and sends the final artifact to Verilator simulation.The Judge can add, replace, or remove testbench entries before simulation compares DUT results with reference outputs.Source: §3.1 · p. 3

3.2 Agentic training framework for RTL verification

• The training framework uses SFT on simulation-validated expert trajectories and GRPO reinforcement learning with verification-specific, agent-wise rewards.Existing RTL datasets are expanded into verified trajectories, while RL uses structured program-tool feedback for end-to-end optimization.Source: §3.2 · p. 4
• GRPO assigns separate composite rewards to the Testcase and FRM agents, including tool-call formatting and functional success signals.The Testcase reward indicates whether the harness runs, while the FRM reward requires all test cases to pass verification; clipped-ratio losses provide critic-free updates.Source: §3.2 · p. 4

4.1 Experimental Setup

• VerilogEval-v2 evaluates viability with Eval0, golden-RTL correctness with Eval1, and fault detection with Eval2-80/90/100.Eval2 uses generated RTL mutants to test whether a testbench identifies faulty implementations at multiple agreement thresholds.Source: §4.1 · p. 5

4.2 Key Results

• 57.7% functional correctness and 34.0% full-mutant robustness are achieved on VerilogEval-v2, while PRO-V-R1 remains competitive with much larger proprietary models.The model attains 57.7% on Eval1 and 34.0% on Eval2-100, with a smaller robustness gap than most baselines.Source: §4.2 · p. 5, Table 2 · p. 5

4.3 Ablation Study

• PRO-V system alone raises performance to 39.1 Eval1 and 28.2 Eval2-100, outperforming CorrectBench at 25.6 and 21.8.The system simplifies the agent’s task to Python generation followed by tool interaction.Source: §4.3 · p. 6
• Post-training further increases Eval0 from 64.7 to 94.9 and reaches 57.7 Eval1 plus 44.2/37.8/34.0 on Eval2-80/90/100.The ablation attributes these gains to the subsequent PRO-V-R1 post-training stage.Source: §4.3 · p. 6, Table 3 · p. 6
• PRO-V-R1 completes verification in 91.2 seconds mean latency versus 805.4 seconds for CorrectBench, yielding an 8.8× speedup.The method generates five Python programs in parallel and typically succeeds within one or two self-consistency iterations.Source: §4.3 · p. 6, Figure 6 · p. 6
• The post-trained model correctly applies Verilog bitwise operations where the base model misinterprets a multibit input as a Python string.Figure 5 presents this semantic-reasoning case study for task 2013_q2afsm.Source: Figure 5 · p. 6, §4.3 · p. 6

• PRO-V-R1 couples an LLM with program-in-the-loop tools, Python-only functional reference modeling, simulation-validated SFT trajectories, and GRPO-based RL.The framework targets automated RTL testbench generation through the PRO-V system.Source: §5 · p. 6
• PRO-V-R1-8B achieves 57.7% Eval1 and 34.0% Eval2-100, surpassing GPT-4o and CorrectBench while delivering an 8.8× speedup.The reported latency is 91 seconds versus 805 seconds per task.Source: §5 · p. 6