# Veritas: Deterministic Verilog Code Synthesis from LLM-Generated Conjunctive Normal Form

arXiv: https://arxiv.org/abs/2506.00005 · HTML: https://mlsanity.com/paper/2506.00005/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 21 references that are in the map.
- First posted on arXiv 7 May 2025.

## Builds on (most cited first, 6 of 6)

- [LoRA: Low-Rank Adaptation of Large Language Models](https://mlsanity.com/paper/2106.09685/) (2021)
- [VerilogEval: Evaluating Large Language Models for Verilog Code Generation](https://mlsanity.com/paper/2309.07544/) (2023)
- [Chip-Chat: Challenges and Opportunities in Conversational Hardware Design](https://mlsanity.com/paper/2305.13243/) (2023)
- [ChipGPT: How far are we from natural language hardware design](https://mlsanity.com/paper/2305.14019/) (2023)
- [AutoChip: Automating HDL Generation Using LLM Feedback](https://mlsanity.com/paper/2311.04887/) (2023)
- [DAVE: Deriving Automatically Verilog from English](https://mlsanity.com/paper/2009.01026/) (2020)

## Built on by (most cited first, 7 of 7)

- [NetDeTox: Adversarial and Efficient Evasion of Hardware-Security GNNs via RL-LLM Orchestration](https://mlsanity.com/paper/2512.00119/) (2025)
- [Large Language Model for Verilog Code Generation: Literature Review and the Road Ahead](https://mlsanity.com/paper/2512.00020/) (2025)
- [CorrectHDL: Agentic HDL Design with LLMs Leveraging High-Level Synthesis as Reference](https://mlsanity.com/paper/2511.16395/) (2025)
- [TrojanGYM: A Detector-in-the-Loop LLM for Adaptive RTL Hardware Trojan Insertion](https://mlsanity.com/paper/2601.17178/) (2026)
- [GUIDE: GenAI Units In Digital Design Education](https://mlsanity.com/paper/2603.17296/) (2026)
- [LLMs for Secure Hardware Design and Related Problems: Opportunities and Challenges](https://mlsanity.com/paper/2605.10807/) (2026)
- [Hardware Design and Security in the Era of Chiplets and LLMs](https://mlsanity.com/paper/2608.05063/) (2026)

## Abstract (arXiv)

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 < 4B), on a dataset of standard RTL components. Experimental results demonstrate that our approach reliably produces functionally correct Verilog code on the first attempt, compared to other lightweight open-source SoTA works such as Verigen (2B parameters) and RTLCoder (4-bit quantized with around 7B parameters). We will release our method and data in full post peer-review.