用推理和形式化验证实现可自动验证的Verilog代码生成
VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification
- 基于推理构建数据集，引导模型生成逻辑正确的硬件代码
- 引入形式化验证框架，确保生成代码在功能上完全正确
- 专为Verilog生成设计的小模型，适合快速原型开发
本文提出VeriThoughts，一个面向基于推理的Verilog代码生成的新数据集。我们建立了一个基于形式化验证方法的新基准框架，用于评估生成硬件描述的质量与正确性。同时，我们提出一系列专门优化的微型模型，专用于Verilog代码生成。该工作回应了自动化硬件设计工具日益增长的需求，能够从高层次规格自动生成可验证正确的实现，有望加速硬件开发流程并保持严格的正确性保障。代码与数据可在https://github.com/wilyub/VeriThoughts获取。
原文摘要 · Abstract (English)
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}.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。