Veritas: Deterministic Verilog Code Synthesis from LLM-Generated Conjunctive Normal Form
Prithwish Basu Roy, Akashdeep Saha, Manaar Alam, Johann Knechtel, Michail Maniatakos, Ozgur Sinanoglu, Ramesh Karri

TL;DR
This paper presents a novel method that uses a lightweight LLM to generate CNF specifications which are then deterministically converted into correct Verilog code, improving reliability and correctness in hardware design synthesis.
Contribution
The paper introduces a CNF-guided synthesis approach that ensures correctness by construction, utilizing a fine-tuned open-source LLM for deterministic Verilog code generation.
Findings
Reliable generation of functionally correct Verilog on first attempt
Outperforms other lightweight open-source synthesis tools
Demonstrates scalability with a small LLM model
Abstract
Automated Verilog code synthesis poses significant challenges and typically demands expert oversight. Traditional high-level synthesis (HLS) methods often fail to scale for real-world designs. While large language models (LLMs) have enhanced scalability, they often introduce syntactical and logical errors requiring extensive post-generation verification. Here, we introduce a novel conjunctive normal form (CNF)-guided synthesis methodology. The idea is to have an LLM generate CNF clauses, a format widely used for formal verification and synthesis validation in hardware design, but here it is used to formally describe the desired circuit functionality. These CNF specifications are then deterministically converted into Verilog, ensuring correctness by construction. Our approach fine-tunes an open-source and lightweight LLM, namely the CPU-deployable LLama-3.2-3B-Instruct model (parameters…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsNatural Language Processing Techniques · Mathematics, Computing, and Information Processing · Handwritten Text Recognition Techniques
