VeriThoughts

https://github.com/wilyub/verithoughts
Admin
VeriThoughts is the first large-scale formally verified Verilog reasoning dataset that enables...
Tokens:7,000
Snippets:57
Trust Score:5.6
Update:5 months ago
Show doc for...
Tokens:
Raw
### Clone Repository and Install Dependencies

Source: https://github.com/wilyub/verithoughts/blob/main/verilog-eval/Verilog_Eval_Test.ipynb

Clones the verilog-eval repository from GitHub, installs it using pip, and installs the Icarus Verilog simulator.

```bash
!git clone https://github.com/NVlabs/verilog-eval/tree/release/1.0.0
!pip install -e verilog-eval
!apt-get update
!apt-get install -y iverilog
```

--------------------------------

### Fine-tune Qwen2.5-7B-Instruct on Reasoning Dataset

Source: https://context7.com/wilyub/verithoughts/llms.txt

Distributed fine-tuning script using LLaMA-Factory and DeepSpeed ZeRO-3 for full-parameter SFT on chain-of-thought Verilog examples. Uses cosine LR scheduling, BF16, and a 16384-token context window across 8 GPUs.

```bash
# Prerequisites: LLaMA-Factory installed, dataset downloaded from HuggingFace
# Dataset files must be placed in: training/verilogFinetune/data/

cd VeriThoughts/training
pip install -r requirements.txt

# Fine-tune Qwen2.5-7B-Instruct on reasoning dataset (8x GPU, ~3 epochs)
chmod +x verilogFinetune/train_qwen_reasoning.sh
./verilogFinetune/train_qwen_reasoning.sh

# Equivalent manual torchrun command:
torchrun \
    --nproc_per_node 8 --nnodes 1 --node_rank 0 \
    --master_addr localhost --master_port 12345 \
    /path/to/LLaMA-Factory/src/train.py \
    --deepspeed verilogFinetune/ds_config_zero3.json \
    --stage sft \
    --do_train \
    --model_name_or_path Qwen/Qwen2.5-7B-Instruct \
    --dataset reasoning_dataset \
    --template qwen \
    --finetuning_type full \
    --output_dir /output/qwen2.5-7b-verilog-reasoning \
    --warmup_steps 100 \
    --learning_rate 8.0e-5 \
    --lr_scheduler_type cosine \
    --per_device_train_batch_size 1 \
    --gradient_accumulation_steps 2 \
    --cutoff_len 16384 \
    --num_train_epochs 3 \
    --bf16

# Available training scripts and their datasets:
# train_qwen_reasoning.sh        -> reasoning_dataset      (Qwen2.5-7B-Instruct)
# train_qwen_reasoning_14b.sh    -> reasoning_dataset      (Qwen2.5-14B-Instruct)
# train_qwen_instruction.sh      -> instruction_dataset    (Qwen2.5-7B-Instruct)
# train_fail_reason_gen.sh       -> fail_reason_gen        (failure augmentation)
# train_fail_reason_gt.sh        -> fail_reason_gt         (failure augmentation)
# train_fail_instruct_gen.sh     -> fail_instruction_gen   (failure augmentation)
# train_fail_instruct_gt.sh      -> fail_instruction_gt    (failure augmentation)
```

--------------------------------

### Run Training Script

Source: https://github.com/wilyub/verithoughts/blob/main/README.md

Execute the training scripts located in the VeriThoughts/training/verilogFinetune directory. Ensure the scripts are executable and all dependencies are installed.

```bash
chmod +x file_name.sh
./file_name.sh
```

--------------------------------

### Run VeriThoughts Dataset Generation Pipeline

Source: https://context7.com/wilyub/verithoughts/llms.txt

Installs dependencies, sets up Yosys, and runs the multi-turn Verilog dataset generation script. Specify start and end indices for processing, batch file path, API keys for Gemini and DeepSeek, and the Yosys installation location.

```bash
cd VeriThoughts/verithoughts
pip install -r requirements.txt

# Install Yosys OSS CAD Suite
# See: https://yosyshq.readthedocs.io/projects/yosys/en/0.41/getting_started/installation.html

# Run dataset generation over indices 0–25090
python multi-turn-yosys-generation.py \
    --start_idx 0 \
    --end_idx 25090 \
    --label_start 0 \
    --batch_file_path /data/verithoughts_output/ \
    --gemini_key AIza... \
    --deepseek_key sk-... \
    --yosys_location /opt/oss-cad-suite/environment
```

--------------------------------

### Install Verilog Eval

Source: https://github.com/wilyub/verithoughts/blob/main/README.md

Clone the verilog-eval repository and install it in editable mode. This is required for running human evaluations.

```bash
git clone https://github.com/NVlabs/verilog-eval/tree/release/1.0.0
pip install -e verilog-eval
```

--------------------------------

### Generate VeriThoughts Dataset

Source: https://github.com/wilyub/verithoughts/blob/main/README.md

Run the VeriThoughts generation script to create the dataset. This script requires specifying start and end indices, batch file path, API keys for language models (Gemini, DeepSeek), and the Yosys installation location.

```python
python multi-turn-yosys-generation.py --start_idx 0 --end_idx 25090 --label_start 0 --batch_file_path your/file/path --gemini_key your_gemini_key --deepseek_key your_deepseek_key --yosys_location your/yosys/location
```

--------------------------------

### Clone VeriThoughts Repository

Source: https://github.com/wilyub/verithoughts/blob/main/README.md

Clone the main VeriThoughts repository and navigate into the verithoughts directory. Ensure you have Git installed.

```bash
git clone https://github.com/wilyub/VeriThoughts.git
cd VeriThoughts/verithoughts
```

--------------------------------

### Navigate to Training Sub-repo

Source: https://github.com/wilyub/verithoughts/blob/main/README.md

Change directory to the training sub-repository within VeriThoughts. This is a prerequisite for training Verilog models.

```bash
cd VeriThoughts/training
```

--------------------------------

### Load and Preprocess Data for Qwen Models

Source: https://github.com/wilyub/verithoughts/blob/main/verilog-eval/Verilog_Eval_Test.ipynb

Loads a JSONL file and preprocesses the 'completion' field to extract Verilog code, handling various potential formatting variations before 'endmodule'. Saves the processed data.

```python
import json
with open('Qwen-2.5-7b-verilog-eval-Human.jsonl','r+') as f:
  data = [json.loads(line) for line in f]
  for item in reversed(data):
    try:
      curr = item['completion'].split("```verilog\n")[1].split("endmodule",1)[0]+"endmodule"
      try:
        curr = item['completion'].split(");\n\n")[1].split("endmodule",1)[0]+"endmodule"
        try:
          curr = item['completion'].split("\n);\n")[1].split("endmodule",1)[0]+"endmodule"
        except:
          pass
      except:
        pass
    except:
      try:
        curr = item['completion'].split("// Your code here\n")[1].split("endmodule",1)[0]+"endmodule"
      except:
        curr = item['completion'].split("endmodule",1)[0]+"endmodule"
    item['completion'] = curr
  f.seek(0)
  json.dump(data, f, indent=4)
  f.truncate()
# write each JSON line back to a new file
with open('test.jsonl','w',encoding='utf8') as f:
    for item in data:
        json.dump(item,f)
        print(file=f) # add a newline
```

--------------------------------

### Load and Preprocess Data for Llama Models

Source: https://github.com/wilyub/verithoughts/blob/main/verilog-eval/Verilog_Eval_Test.ipynb

Loads a JSONL file, preprocesses the 'completion' field by extracting Verilog code up to 'endmodule', and saves the modified data back to the file and a new 'test.jsonl' file.

```python
import json
with open('RTLCoder-v1.1-verilog-eval-Human.jsonl','r+') as f:
  data = [json.loads(line) for line in f]
  for item in reversed(data):
    curr = item['completion'].split("endmodule",1)[0]+"endmodule"
    item['completion'] = curr
  f.seek(0)
  json.dump(data, f, indent=4)
  f.truncate()
# write each JSON line back to a new file
with open('test.jsonl','w',encoding='utf8') as f:
    for item in data:
        json.dump(item,f)
        print(file=f) # add a newline
```

--------------------------------

### Navigate to Verilog-Eval Directory

Source: https://github.com/wilyub/verithoughts/blob/main/verilog-eval/Verilog_Eval_Test.ipynb

Changes the current working directory to the cloned verilog-eval directory on Google Drive.

```python
%cd /content/drive/MyDrive/verilog-eval/
```

--------------------------------

### Load and Preprocess Data for Closed-Source Models

Source: https://github.com/wilyub/verithoughts/blob/main/verilog-eval/Verilog_Eval_Test.ipynb

Loads a JSONL file and preprocesses the 'completion' field to extract Verilog code, attempting to handle various common code block delimiters before 'endmodule'. Saves the processed data.

```python
import json
with open('gpt-4o-verilog-eval-Human.jsonl','r+') as f:
  data = [json.loads(line) for line in f]
  for item in reversed(data):
    try:
          curr = item['completion'].split("\n);\n")[1].split("endmodule",1)[0]+"endmodule"
    except:
      try:
        curr = item['completion'].split("```verilog\n")[1].split("endmodule",1)[0]+"endmodule"
      except:
        try:
          curr = item['completion'].split("// Your code here\n")[1].split("endmodule",1)[0]+"endmodule"
        except:
         curr = item['completion'].split("endmodule",1)[0]+"endmodule"
    item['completion'] = curr
  f.seek(0)
  json.dump(data, f, indent=4)
  f.truncate()
# write each JSON line back to a new file
with open('test.jsonl','w',encoding='utf8') as f:
    for item in data:
        json.dump(item,f)
        print(file=f) # add a newline
```

--------------------------------

### Generate Completions for VerilogEval Benchmark with vLLM

Source: https://context7.com/wilyub/verithoughts/llms.txt

Script to generate completions for the NVlabs VerilogEval benchmark (Human or Machine split) using a local vLLM-served model. Outputs a JSONL file compatible with the `verilog-eval` scoring library.

```bash
cd VeriThoughts/verilog-eval
pip install -r requirements.txt
git clone https://github.com/NVlabs/verilog-eval/tree/release/1.0.0
pip install -e verilog-eval

# Evaluate on VerilogEval-Human benchmark (GPU 0)
python verilog_eval_generate_vllm.py \
    --model_id nyu-dice-lab/Qwen-2.5-Instruct-Verilog-Reasoning-7B \
    --gpu 0 \
    --bench_type Human \
    --hf_token hf_...

# Output: /outputs/nyu-dice-lab/Qwen-2.5-Instruct-Verilog-Reasoning-7B-verilog-eval-Human.jsonl
# Each entry: {"task_id": "Prob001_notgate", "completion": "assign out = ~in;\nendmodule"}

# Then follow Verilog_Eval_Test.ipynb to compute pass@k scores
```

--------------------------------

### Navigate to Verilog Eval Human Sub-repo

Source: https://github.com/wilyub/verithoughts/blob/main/README.md

Change directory to the verilog-eval sub-repository. This is used for human evaluation of Verilog code generation.

```bash
cd VeriThoughts/verilog-eval
```

--------------------------------

### Generate Benchmark Responses for Verilog Eval Human

Source: https://github.com/wilyub/verithoughts/blob/main/README.md

Generate benchmark responses for human evaluation using a specified model and GPU. Requires model ID, GPU index, benchmark type, and Hugging Face token.

```python
python verilog_eval_generate_vllm.py --model_id your/model/id --gpu 0 --bench_type human --hf_token my_hf_token
```

--------------------------------

### Run Yosys Formal Equivalence Check

Source: https://context7.com/wilyub/verithoughts/llms.txt

Writes Verilog files, creates a Yosys script for miter circuit construction, and runs formal verification over 50 time steps. Returns a list of return codes indicating equivalence (0), failure (1), or error (-1).

```python
import subprocess, os

generated_code = """
module adder(input [3:0] a, b, output [4:0] sum);
    assign sum = a + b;
endmodule
"""

ground_truth = """
module adder(input [3:0] a, b, output [4:0] sum);
    assign sum = {1'b0, a} + {1'b0, b};
endmodule
"""

stdout_list = create_yosys_files(
    batch_file_path="/tmp/yosys_workspace/",
    initial_code=generated_code,
    ground_truth=ground_truth
)

# stdout_list = [0]  ->  all modules verified equivalent
# stdout_list = [1]  ->  equivalence check failed (counterexample found)
# stdout_list = [-1] ->  timeout or subprocess error

verified = all(rc == 0 for rc in stdout_list)
print("Formally verified:", verified)  # True
```

--------------------------------

### DeepSpeed ZeRO Stage 3 Configuration

Source: https://context7.com/wilyub/verithoughts/llms.txt

Configuration for DeepSpeed ZeRO Stage 3, enabling memory-efficient distributed training by sharding optimizer states, gradients, and model parameters. Suitable for training large models on multi-GPU nodes.

```json
{
  "train_batch_size": "auto",
  "train_micro_batch_size_per_gpu": "auto",
  "gradient_accumulation_steps": "auto",
  "bf16": { "enabled": "auto" },
  "zero_optimization": {
    "stage": 3,
    "overlap_comm": true,
    "contiguous_gradients": true,
    "sub_group_size": 1e9,
    "reduce_bucket_size": "auto",
    "stage3_prefetch_bucket_size": "auto",
    "stage3_param_persistence_threshold": "auto",
    "stage3_max_live_parameters": 1e9,
    "stage3_max_reuse_distance": 1e9,
    "stage3_gather_16bit_weights_on_model_save": true
  }
}
```

--------------------------------

### Navigate to VeriThoughts Evaluation Sub-repo

Source: https://github.com/wilyub/verithoughts/blob/main/README.md

Change directory to the evaluation_verithoughts sub-repository. This is where you will run scripts to generate and evaluate benchmark responses.

```bash
cd VeriThoughts/evaluation_verithoughts
```

--------------------------------

### Batch Inference on VeriThoughts Benchmark with vLLM

Source: https://context7.com/wilyub/verithoughts/llms.txt

Script for batch inference on the VeriThoughts benchmark using vLLM. It loads a fine-tuned model, filters for formally-verified questions, and generates multiple completions per question. Supports reasoning mode and multi-GPU tensor parallelism.

```bash
cd VeriThoughts/evaluation_verithoughts
pip install -r requirements.txt

# Generate 20 samples per question with reasoning mode (4 GPUs)
python verilog_vllm_multi.py \
    --model_id nyu-dice-lab/Qwen-2.5-Instruct-Verilog-Reasoning-7B \
    --sample_number 20 \
    --batch_size 100 \
    --reasoning_mode \
    --hf_read_token hf_... \
    --benchmark_path /data/verithoughts_benchmark.jsonl \
    --tensor_parallel_size 4

# Output: benchmark_results/nyu-dice-lab/Qwen-2.5-Instruct-Verilog-Reasoning-7B/results.jsonl
# Each JSONL entry:
# {
#   "question": "Write a Verilog module 'counter' with ...",
#   "full_response": "<think>...</think>\nCODE BEGIN\nmodule counter...\nCODE END",
#   "generated_code": "\nmodule counter(...); ... \n",
#   "ground_truth": "module counter(...); ..."
# }
```

--------------------------------

### Evaluate Functional Correctness (Llama)

Source: https://github.com/wilyub/verithoughts/blob/main/verilog-eval/Verilog_Eval_Test.ipynb

Runs the functional correctness evaluation using the 'evaluate_functional_correctness' tool with the preprocessed 'test.jsonl' file and the specified problem file.

```bash
!evaluate_functional_correctness ./test.jsonl --problem_file=/content/drive/MyDrive/verilog-eval/data/VerilogEval_Human.jsonl
```

--------------------------------

### Evaluate Claude 3.7 Sonnet with VerilogEval

Source: https://context7.com/wilyub/verithoughts/llms.txt

This script evaluates the Claude 3.7 Sonnet model against the VerilogEval benchmark. It requires the ANTHROPIC_API_KEY environment variable to be set.

```python
# verilog_eval_vllm_claude.py — evaluate Claude 3.7 Sonnet
import anthropic, os

client = anthropic.Anthropic(api_key=os.environ["ANTHROPIC_API_KEY"])

# Single completion for one VerilogEval problem
response = client.messages.create(
    model="claude-3-7-sonnet-20250219",
    max_tokens=16384,
    messages=[
        {
            "role": "user",
            "content": "Implement a Verilog module 'mux4to1' with 4 data inputs d[3:0], "
                       "2-bit select s[1:0], and output y.\nmodule mux4to1(\n"
        }
    ]
)
completion = response.content[0].text
```

```bash
# Run full benchmark:
python verilog-eval/closed-source/verilog_eval_vllm_claude.py --bench_type Human
# python verilog-eval/closed-source/verilog_eval_vllm_gemini.py --bench_type Human
# python verilog-eval/closed-source/verilog_eval_vllm_gpt-4o.py --bench_type Human
# python verilog-eval/closed-source/verilog_eval_vllm_gpt-o3.py --bench_type Human
```

--------------------------------

### Mount Google Drive

Source: https://github.com/wilyub/verithoughts/blob/main/verilog-eval/Verilog_Eval_Test.ipynb

Mounts Google Drive to the Colab environment. This is necessary to access files stored on Drive.

```python
from google.colab import drive
drive.mount('/content/drive')
```

--------------------------------

### Formal Pass@k Evaluation with Yosys

Source: https://context7.com/wilyub/verithoughts/llms.txt

Script to perform formal pass@k evaluation on generated Verilog code using Yosys. It parses JSONL results, extracts Verilog code, and checks equivalence against ground truth. Requires prior generation of results using `verilog_vllm_multi.py`.

```bash
# Run after generating responses with verilog_vllm_multi.py
python evaluation_script.py \
    --results_path benchmark_results/nyu-dice-lab/Qwen-2.5-Instruct-Verilog-Reasoning-7B/results.jsonl \
    --samples_per_question 20 \
    --yosys_location /opt/oss-cad-suite/environment \
    --benchmark_path /data/verithoughts_benchmark.jsonl

# Example output:
# pass@1:  0.612
# pass@5:  0.784
# pass@10: 0.831

# For reasoning models (parses CODE BEGIN/END before module extraction):
python evaluation_script.py \
    --results_path results.jsonl \
    --samples_per_question 20 \
    --reason_mode \
    --yosys_location /opt/oss-cad-suite/environment \
    --benchmark_path /data/verithoughts_benchmark.jsonl
```

--------------------------------

### Generate Benchmark Responses for VeriThoughts Evaluation

Source: https://github.com/wilyub/verithoughts/blob/main/README.md

Generate benchmark responses using a specified model and reasoning mode. Requires model ID, sample number, batch size, reasoning mode flag, Hugging Face token, benchmark path, and tensor parallel size.

```python
python verilog_vllm_multi.py --model_id nyu-dice-lab/Qwen-2.5-Instruct-Verilog-Reasoning-7B --sample_number 20 --batch_size 100 --reasoning_mode --hf_read_token your_hf_token --benchmark_path  your_benchmark_path --tensor_parallel_size 4
```

--------------------------------

### Change Directory to Drive

Source: https://github.com/wilyub/verithoughts/blob/main/verilog-eval/Verilog_Eval_Test.ipynb

Changes the current working directory to the Google Drive 'MyDrive' folder. This is often a prerequisite for subsequent file operations.

```python
%cd /content/drive/MyDrive
```

--------------------------------

### Rate-Limit-Aware Gemini API Wrapper

Source: https://context7.com/wilyub/verithoughts/llms.txt

Handles Google Gemini API rate limits (429) and server errors (502/503) with exponential backoff and retries. Parses `retryDelay` from error responses. Supports custom retry limits via a decorator.

```python
from multi_turn_yosys_generation import retry_on_rate_limit, safe_gemini_send
from google import genai
from google.genai import types

gemini_client = genai.Client(api_key="AIza...")
chat = gemini_client.chats.create(model="gemini-2.0-flash-thinking-exp")

# safe_gemini_send automatically retries on 429 / 502 / 503
response = safe_gemini_send(
    chat,
    "Write a Verilog module for a D flip-flop with synchronous reset.",
    config=types.GenerateContentConfig(
        max_output_tokens=8192,
        temperature=0.6,
        topP=0.95,
    )
)
print(response.text)
# "CODE BEGIN\nmodule dff(...); ... CODE END"

# Custom retry limit:
@retry_on_rate_limit(max_retries=10)
def my_api_call(chat, msg):
    return chat.send_message(msg)
```

--------------------------------

### Evaluate VeriThoughts Benchmark Responses

Source: https://github.com/wilyub/verithoughts/blob/main/README.md

Evaluate the generated benchmark responses. This script requires the path to the generated results, number of samples per question, Yosys location, and the benchmark path.

```python
python evaluation_script.py --results_path your/generated/jsonl --samples_per_question 20 --yosys_location your/yosys/location --benchmark_path your/benchmark/path
```

--------------------------------

### Extract Verilog Code from LLM Output

Source: https://context7.com/wilyub/verithoughts/llms.txt

Parses LLM responses to extract Verilog code enclosed by 'CODE BEGIN' and 'CODE END' markers. Returns the extracted code or an empty string if no delimiters are found. Useful for processing model outputs containing chain-of-thought reasoning.

```python
from multi_turn_yosys_generation import extract_code_block

# LLM response with chain-of-thought reasoning and delimited code
llm_response = """
<think>
We need to implement a 2-to-1 multiplexer...
</think>
Here is the implementation:
CODE BEGIN
module mux2to1(input a, b, sel, output y);
    assign y = sel ? b : a;
endmodule
CODE END
"""

code = extract_code_block(llm_response)
print(code)
# Output:
#
# module mux2to1(input a, b, sel, output y);
#     assign y = sel ? b : a;
# endmodule
#

# Returns empty string if no delimiters found
print(extract_code_block("Just some text"))  # ""
```

--------------------------------

### Rename Verilog Modules for Yosys Equivalence Check

Source: https://context7.com/wilyub/verithoughts/llms.txt

Appends '1' to all Verilog module declarations and instantiations. This is necessary for Yosys's formal equivalence checking, which requires distinct names for the ground-truth and generated modules to create a miter circuit.

```python
from multi_turn_yosys_generation import rename_modules_and_instantiations

ground_truth_verilog = """
module full_adder(input a, b, cin, output sum, cout);
    assign {cout, sum} = a + b + cin;
endmodule

module ripple_adder(input [3:0] a, b, input cin, output [3:0] sum, output cout);
    wire c1, c2, c3;
    full_adder fa0(a[0], b[0], cin,  sum[0], c1);
    full_adder fa1(a[1], b[1], c1,   sum[1], c2);
    full_adder fa2(a[2], b[2], c2,   sum[2], c3);
    full_adder fa3(a[3], b[3], c3,   sum[3], cout);
endmodule
"""

renamed_code, rename_map = rename_modules_and_instantiations(ground_truth_verilog)
print(rename_map)
# {'full_adder': 'full_adder1', 'ripple_adder': 'ripple_adder1'}
```

--------------------------------

### Unbiased Pass@k Metric Calculation

Source: https://context7.com/wilyub/verithoughts/llms.txt

Python function to compute the standard pass@k metric. It takes a list of correct counts per question, the total number of samples per question, and the k value to calculate an unbiased estimate using a combinatorial formula.

```python
from evaluation_script import pass_at_k

# 100 questions, each sampled 20 times
# correct_counts[i] = how many of 20 samples for question i passed Yosys check
correct_counts = [15, 0, 20, 8, 3, 20, 12, 0, 7, 18]  # ... 90 more

p1  = pass_at_k(correct_counts, n=20, k=1)
p5  = pass_at_k(correct_counts, n=20, k=5)
p10 = pass_at_k(correct_counts, n=20, k=10)

print(f"pass@1:  {p1:.3f}")   # pass@1:  0.612
print(f"pass@5:  {p5:.3f}")   # pass@5:  0.784
print(f"pass@10: {p10:.3f}")  # pass@10: 0.831
```
Tokens:
Raw