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

Chinmay Hegde (New York University) · Patrick Yubeaton (New York University) · Andre Nakkab (New York University) · Weihua Xiao (New York University) · Luca Collini (New York University) · Ramesh Karri (New York University) · Siddharth Garg (NYU)
automated hardware designbenchmark frameworkcode generation techniquescorrectness guaranteesevaluation metricsformal verificationhardware descriptionshardware developmenthigh-level specificationsreasoning-based generationsmall-scale modelsspecialized modelsverifiably correct implementationsverilog codeverithoughts

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.