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

arXiv: https://arxiv.org/abs/2506.12200 · HTML: https://mlsanity.com/paper/2506.12200/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning for agents, planning and code, one of 17 directions in LLM reasoning.
- Builds on 15 of its 41 references that are in the map.
- First posted on arXiv 13 Jun 2025.

## Placed in

- LLM reasoning / [Reasoning for agents, planning and code](https://mlsanity.com/lr/reasoning-for-agents-planning-and-code/)
- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

## Builds on (most cited first, 15 of 15)

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Toolformer: Language Models Can Teach Themselves to Use Tools](https://mlsanity.com/paper/2302.04761/) (2023)
- [WebArena: A Realistic Web Environment for Building Autonomous Agents](https://mlsanity.com/paper/2307.13854/) (2023)
- [Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Tasks](https://mlsanity.com/paper/2211.12588/) (2022)
- [The AI Scientist: Towards Fully Automated Open-Ended Scientific Discovery](https://mlsanity.com/paper/2408.06292/) (2024)
- [PAL: Program-aided Language Models](https://mlsanity.com/paper/2211.10435/) (2022)
- [ChemCrow: Augmenting large-language models with chemistry tools](https://mlsanity.com/paper/2304.05376/) (2023)
- [Revisiting VerilogEval: A Year of Improvements in Large-Language Models for Hardware Code Generation](https://mlsanity.com/paper/2408.11053/) (2024)
- [CodeV: Empowering LLMs with HDL Generation through Multi-Level Summarization](https://mlsanity.com/paper/2407.10424/) (2024)
- [QiMeng-CodeV-R1: Reasoning-Enhanced Verilog Generation](https://mlsanity.com/paper/2505.24183/) (2025)
- [CorrectBench: Automatic Testbench Generation with Functional Self-Correction using LLMs for HDL Design](https://mlsanity.com/paper/2411.08510/) (2024)
- [EAGLE: Efficient Adaptive Geometry-based Learning in Cross-view Understanding](https://mlsanity.com/paper/2406.01429/) (2024)
- [StringLLM: Understanding the String Processing Capability of Large Language Models](https://mlsanity.com/paper/2410.01208/) (2024)

## Built on by (most cited first, 7 of 7)

- [LLM4Cov: Execution-Aware Agentic Learning for High-coverage Testbench Generation](https://mlsanity.com/paper/2602.16953/) (2026)
- [Faver: Boosting LLM-based RTL Generation with Function Abstracted Verifiable Middleware](https://mlsanity.com/paper/2510.08664/) (2025)
- [Agentic Electronic Design Automation: A Handoff Perspective](https://mlsanity.com/paper/2606.19795/) (2026)
- [AgentDV: Closed-Loop Agentic AI for Hardware Design Verification](https://mlsanity.com/paper/2608.27148/) (2026)
- [CovR: Coverage-Aware Hardware Verification via Reasoning-Guided Reinforcement Learning](https://mlsanity.com/paper/2609.19189/) (2026)
- [BEHAVE: Functional Behavior Modeling Enables Self-Improving Agents for Hardware Design and Verification](https://mlsanity.com/paper/2609.34785/) (2026)
- [A Survey on LLM-Integrated Hardware Design Verification](https://mlsanity.com/paper/2610.10580/) (2026)

## Abstract (arXiv)

Register-Transfer Level (RTL) verification is a primary bottleneck, consuming 60-70% of development time. While Large Language Models (LLMs) show promise for RTL automation, their performance and research focus have overwhelmingly centered on RTL generation rather than verification. Current methods for RTL verification rely on large scale proprietary models (e.g., GPT-4o) to generate Python-based functional references, incurring a high cost and raising data-privacy risks. To date, an end-to-end open-source solution for autonomous verification remains absent. We introduce PRO-V-R1, the first trainable open-source agentic framework for autonomous RTL verification. Our contributions are threefold: (1) we design PRO-V sys, a modular agentic system that couples LLM-based reasoning with programmatic tool use for RTL verification; (2) we establish a data construction pipeline that leverages existing RTL datasets to build simulation-validated, expert-level trajectories tailored for supervised fine-tuning (SFT) RTL verification agents; and (3) we implement an efficient reinforcement learning (RL) algorithm that uses verification-specific rewards derived from program-tool feedback to optimize the end-to-end verification workflow. Our empirical evaluation demonstrates PRO-V-R1 achieves a 57.7% functional correctness rate and 34.0% in robust fault detection, significantly outperforming the base model's 25.7% and 21.8% (respectively) from the state-of-the-art (SOTA) automatic verification system. This configuration also outperforms large-scale proprietary LLMs in functional correctness and shows comparable robustness for fault detection.