Research map / Large language models / Agents, code and math

VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification

NeurIPS 2025 · Large language models › Agents, code and math · approach: Retrieval-augmented formal theorem proving · 2 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Introduces VeriThoughts, a ~20K-sample formally verified Verilog reasoning dataset built from MetRex with Gemini-generated questions and DeepSeek-R1 reasoning traces, and fine-tunes Qwen2.5-14B reasoning models that set open-source results on VerilogEval.

Problem

LLM Verilog code generation lacks large-scale question-code-reasoning data, and existing evaluations rely on weak testbench simulation rather than formal equivalence checking.

Approach

Generate natural-language questions for synthesizable Verilog, regenerate Verilog with a reasoning model, and use Yosys-based formal equivalence checking as a self-consistency label for question-answer quality; use the resulting data for SFT of reasoning models and a formally verified benchmark.

Key results

• VeriThoughts-14B reaches 43.7% pass@1 on VerilogEval Human, the highest among open-source models reported, and 78.5% pass@1 on the VeriThoughts benchmark.
• Reasoning-trace SFT on self-consistent data beats instruct SFT by 26.5 points pass@1 on VeriThoughts (75.5% vs 49.0%).
• Manual analysis of 100 samples found 0 errors among 50 self-consistent samples and 66% question errors among 50 inconsistent samples.

Measured effects reported in the paper

Surprising findings

• Models trained on inconsistent (Q, V*) pairs outperformed models trained on self-consistent pairs on nearly all evaluations, suggesting hallucinated question-answer pairs can still be useful.
• On VerilogEval, the reasoning model trained on self-consistent data gained nothing from consistency filtering at any pass@k level.

Limitations

• Formal verification check via Yosys cannot distinguish question errors from code-generation errors, so the self-consistency label is only a proxy.
• Dataset is built solely from MetRex, limiting diversity of Verilog sources.
• Fine-tuning subsets are small (~10K samples) and results for some models are missing due to compute constraints.

Experimental setup

Datasets: MetRex VeriThoughts VerilogEval

Benchmarks: VerilogEval VeriThoughts benchmark

Metrics: pass@1 pass@5 pass@10

Baselines: VerilogEval CL-Verilog RTLCoder DeepSeek-R1-Distill-Qwen-14B Qwen3-14B GPT-4o Claude 3.7 Sonnet ChatGPT-o3 Gemini-2.5-Flash-Preview-04-17

Builds on: MetRex VerilogEval LLaMA-Factory DeepSeek-R1

Closest papers by meaning

• BetterV: Controlled Verilog Generation with Discriminative Guidance (ICML 2024 · similarity 0.89)
• VerilogCoder: Autonomous Verilog Coding Agents with Graph-based Planning and Abstract Syntax Tree (AST)-based Waveform Tracing Tool (AAAI 2025 · similarity 0.89)
• CraftRTL: High-quality Synthetic Data Generation for Verilog Code Models with Correct-by-Construction Non-Textual Representations and Targeted Code Repair (ICLR 2025 · similarity 0.88)
• HierSVA: A Synthesis Pipeline, Dataset, and Benchmark for LLM-Driven Hierarchical Hardware Formal Verification (NeurIPS 2026 · similarity 0.87)
• QiMeng-CodeV-R1: Reasoning-Enhanced Verilog Generation (NeurIPS 2025 · similarity 0.87)
• QiMeng-SALV: Signal-Aware Learning for Verilog Code Generation (NeurIPS 2025 · similarity 0.86)