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

• URL: http://arxiv.org/abs/2505.20302v2
• Date: Sat, 07 Jun 2025 23:58:45 GMT
• Title: VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification
• Abstract summary: This paper introduces VeriThoughts, a novel dataset designed for reasoning-based Verilog code generation.<n>We establish a new benchmark framework grounded in formal verification methods to evaluate the quality and correctness of generated hardware descriptions.<n>We present a suite of specialized small-scale models optimized specifically for Verilog generation.
• Score: 28.196015311346024
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This paper introduces VeriThoughts, a novel dataset designed for reasoning-based Verilog code generation. We establish a new benchmark framework grounded in formal verification methods to evaluate the quality and correctness of generated hardware descriptions. Additionally, we present a suite of specialized small-scale models optimized specifically for Verilog generation. Our work addresses the growing need for automated hardware design tools that can produce verifiably correct implementations from high-level specifications, potentially accelerating the hardware development process while maintaining rigorous correctness guarantees. Our code and data are available at \href{https://github.com/wilyub/VeriThoughts}{this URL}.

Related papers

• WybeCoder: Verified Imperative Code Generation [22.401681809856896]
  WybeCoder is an agentic code verification framework.<n>It enables prove-as-you-generate development where code, invariants, and proofs co-evolve.
  arXiv  Detail & Related papers  (2026-03-31T00:06:44Z)
• QiMeng-CRUX: Narrowing the Gap between Natural Language and Verilog via Core Refined Understanding eXpression [48.84841760215598]
  Large language models (LLMs) have shown promising capabilities in hardware description language (HDL) generation.<n>Existing approaches often rely on free-form natural language descriptions that are often ambiguous, redundant, and unstructured.<n>We treat hardware code generation as a complex transformation from an open-ended natural language space to a domain-specific, highly constrained target space.<n>We introduce Core Refined Understanding eXpression (CRUX), a structured intermediate space that captures the essential semantics of user intent while organizing the expression for precise Verilog code generation.
  arXiv  Detail & Related papers  (2025-11-25T09:17:32Z)
• Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking [54.43083499412643]
  Test-time algorithms that combine the generative power of language models with process verifiers offer a promising lever for eliciting new reasoning capabilities.<n>We introduce a new process-guided test-time sampling algorithm, VGB, which uses theoretically grounded backtracking to achieve provably better robustness to verifier errors.
  arXiv  Detail & Related papers  (2025-10-03T16:21:14Z)
• VeriGRAG: Enhancing LLM-Based Verilog Code Generation with Structure-Aware Soft Prompts [4.227182480042518]
  We propose a novel framework that extracts structural graph embeddings from Verilog code using graph neural networks (GNNs)<n>A multimodal retriever then selects the graph embeddings most relevant to the given generation task.<n>Experiments demonstrate that VeriGRAG substantially improves the correctness of Verilog code generation.
  arXiv  Detail & Related papers  (2025-09-27T10:23:36Z)
• VERINA: Benchmarking Verifiable Code Generation [47.9771074559674]
  Large language models (LLMs) are increasingly integrated in software development.<n>Verifiable code generation offers a promising path to address this limitation.<n>Current benchmarks often lack support for end-to-end verifiable code generation.
  arXiv  Detail & Related papers  (2025-05-29T06:12:52Z)
• Paper2Code: Automating Code Generation from Scientific Papers in Machine Learning [57.09163579304332]
  We introduce PaperCoder, a framework that transforms machine learning papers into functional code repositories.<n>PaperCoder operates in three stages: planning, designs the system architecture with diagrams, identifies file dependencies, and generates configuration files.<n>We then evaluate PaperCoder on generating code implementations from machine learning papers based on both model-based and human evaluations.
  arXiv  Detail & Related papers  (2025-04-24T01:57:01Z)
• Insights from Verification: Training a Verilog Generation LLM with Reinforcement Learning with Testbench Feedback [36.69082579950107]
  Large language models (LLMs) have shown strong performance in Verilog generation from natural language description.<n>This paper introduces a method that integrates verification insights from testbench into the training of Verilog generation LLMs.
  arXiv  Detail & Related papers  (2025-04-22T11:38:14Z)
• VeriMind: Agentic LLM for Automated Verilog Generation with a Novel Evaluation Metric [4.590930025882158]
  We propose VeriMind, an agentic LLM framework for Verilog code generation.<n>We introduce a novel evaluation metric-pass@ARC-which combines the conventional pass@k measure with Average Refinement Cycles (ARC) to capture both success rate and the efficiency of iterative refinement.<n> Experimental results on diverse hardware design tasks demonstrated that our approach achieved up to $8.3%$ improvement on pass@k metric and $8.1%$ on pass@ARC metric.
  arXiv  Detail & Related papers  (2025-03-15T23:43:06Z)
• Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
  We present the Code-Development Benchmark (Codev-Bench), a fine-grained, real-world, repository-level, and developer-centric evaluation framework. Codev-Agent is an agent-based system that automates repository crawling, constructs execution environments, extracts dynamic calling chains from existing unit tests, and generates new test samples to avoid data leakage.
  arXiv  Detail & Related papers  (2024-10-02T09:11:10Z)
• VerilogCoder: Autonomous Verilog Coding Agents with Graph-based Planning and Abstract Syntax Tree (AST)-based Waveform Tracing Tool [4.027984601764008]
  We propose VerilogCoder, a system of multiple Artificial Intelligence (AI) agents for Verilog code generation.<n>The proposed methodology successfully generates 94.2% syntactically and functionally correct Verilog code.
  arXiv  Detail & Related papers  (2024-08-15T20:06:06Z)
• Data is all you need: Finetuning LLMs for Chip Design via an Automated design-data augmentation framework [50.02710905062184]
  This paper proposes an automated design-data augmentation framework, which generates high-volume and high-quality natural language aligned with Verilog and EDA scripts. The accuracy of Verilog generation surpasses that of the current state-of-the-art open-source Verilog generation model, increasing from 58.8% to 70.6% with the same benchmark.
  arXiv  Detail & Related papers  (2024-03-17T13:01:03Z)
• BetterV: Controlled Verilog Generation with Discriminative Guidance [11.162807308782751]
  We propose a Verilog generation framework, BetterV, which fine-tunes the large language models (LLMs) on processed domain-specific runtime. BetterV has the ability to generate syntactically and functionally correct Verilog, which can outperform GPT-4 on the VerilogEval benchmark.
  arXiv  Detail & Related papers  (2024-02-03T08:00:12Z)
• VerilogEval: Evaluating Large Language Models for Verilog Code Generation [6.88526119890374]
  We present a comprehensive evaluation dataset consisting of 156 problems from the Verilog instructional website HDLBits. The evaluation set consists of a diverse set of Verilog code generation tasks, ranging from simple combinational circuits to complex finite state machines.
  arXiv  Detail & Related papers  (2023-09-14T09:15:34Z)
• ReCode: Robustness Evaluation of Code Generation Models [90.10436771217243]
  We propose ReCode, a comprehensive robustness evaluation benchmark for code generation models. We customize over 30 transformations specifically for code on docstrings, function and variable names, code syntax, and code format. With human annotators, we verified that over 90% of the perturbed prompts do not alter the semantic meaning of the original prompt.
  arXiv  Detail & Related papers  (2022-12-20T14:11:31Z)
• CodeExp: Explanatory Code Document Generation [94.43677536210465]
  Existing code-to-text generation models produce only high-level summaries of code. We conduct a human study to identify the criteria for high-quality explanatory docstring for code. We present a multi-stage fine-tuning strategy and baseline models for the task.
  arXiv  Detail & Related papers  (2022-11-25T18:05:44Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.