Generate correct CNF equations for digital designs (adder, subtractor, multiplexer, multiplier, decoder) and seamlessly convert them all the way to .bench and Verilog (.v)—with a simple CLI workflow.

Veritas leverages the idea that a correct CNF can always be converted to correct Verilog that does not require further testing.

• CNF generation for common building blocks
• CNF → .bench conversion
• .bench simulation (truth-table style)
• .bench → Verilog conversion
• Simple, incremental prompting workflow (via gpt-5-mini by default)

Requires Python 3.8+

Install the OpenAI Python package:

pip install openai

(If you use virtual environments, activate one first.)

1. Generate a CNF for a design using cli.py
2. Convert CNF → .bench with CNF_to_bench.py
3. Simulate the .bench with bench_simulator.py (optional)
4. Convert .bench → Verilog with bench2verilog.py

cli.py incrementally queries an LLM to produce a correct CNF for the chosen design and configuration. This may take a few minutes because it performs multiple LLM interactions to validate the result.

Usage

python cli.py --key <openai_api_key> --design <design name> --type <configuration>

Supported designs & configurations

Example

python cli.py --key <openai_api_key> --design subtractor --type 3-bit
# Output: subtractor_3-bit.cnf

Output filenames follow the pattern: <design>_<type>.cnf

Convert the generated CNF file into a .bench netlist.

Usage

python CNF_to_bench.py --cnf <design_type.cnf>   --inputs "<comma-separated input names>"   --outputs "<comma-separated output names>"   --out <design_type.bench>

Example

python CNF_to_bench.py --cnf subtractor_3-bit.cnf   --inputs "A0,B0,A1,B1,A2,B2,Din"   --outputs "D0,D1,D2,S2"   --out subtractor_3-bit.bench
# Output: subtractor_3-bit.bench

Simulate the .bench file to verify expected behavior (optionally produce a table).

Usage

python bench_simulator.py --bench <design_type.bench> --table --inputs <comma-separated input names>

Example

python bench_simulator.py --bench subtractor_3-bit.bench --table --inputs A0,B0,A1,B1,A2,B2,Din

Convert a .bench file into an equivalent Verilog module.

Usage

python bench2verilog.py --bench <design_type.bench> --out <design_type.v>

Example

python bench2verilog.py --bench subtractor_3-bit.bench --out subtractor_3-bit.v

• Ensure your OpenAI API key is available and valid (--key flag).
• Input and output signal names must match the CNF variables when converting to .bench.
• If you run into environment issues, try an isolated virtual environment:

  python -m venv .venv && source .venv/bin/activate

• GitHub: https://github.com/PrithwishBasuRoy/Veritas
• arXiv (PDF): https://arxiv.org/pdf/2506.00005

If you use Veritas in your research, please cite:

@misc{roy2025veritasdeterministicverilogcode,
      title={Veritas: Deterministic Verilog Code Synthesis from LLM-Generated Conjunctive Normal Form}, 
      author={Prithwish Basu Roy and Akashdeep Saha and Manaar Alam and Johann Knechtel and Michail Maniatakos and Ozgur Sinanoglu and Ramesh Karri},
      year={2025},
      eprint={2506.00005},
      archivePrefix={arXiv},
      primaryClass={cs.AR},
      url={https://arxiv.org/abs/2506.00005}, 
}