Enhancing Large Language Models for Hardware Verification: A Novel SystemVerilog Assertion Dataset

TL;DR

VERT provides an open-source, domain-focused dataset to fine-tune open-source LLMs for SystemVerilog assertion generation, addressing clock-cycle interpretation, conditional dependencies, nested logic, and long-condition handling that challenge SOTA models. By combining synthetic data with targeted variables from real HDL projects and applying LoRA-based fine-tuning, DeepSeek Coder and Llama 3.1 achieve substantial gains in both syntactic and functional correctness—up to $96.88\%$ improvements over base models and up to $24.14\%$ over GPT-4o—across industry benchmarks OpenTitan, CVA6, OpenPiton, and Pulpissimo. The study also performs data leakage checks, ablation with uncleaned variable names, and contamination analyses, demonstrating robust generalization and outlining pathways for integration with verification tools. Overall, VERT demonstrates that domain-specific datasets can unlock the potential of smaller, open-source models to outperform licensed giants in hardware verification tasks, offering privacy-preserving, scalable verification automation.

Abstract

Hardware verification is crucial in modern SoC design, consuming around 70% of development time. SystemVerilog assertions ensure correct functionality. However, existing industrial practices rely on manual efforts for assertion generation, which becomes increasingly untenable as hardware systems become complex. Recent research shows that Large Language Models (LLMs) can automate this process. However, proprietary SOTA models like GPT-4o often generate inaccurate assertions and require expensive licenses, while smaller open-source LLMs need fine-tuning to manage HDL code complexities. To address these issues, we introduce **VERT**, an open-source dataset designed to enhance SystemVerilog assertion generation using LLMs. VERT enables researchers in academia and industry to fine-tune open-source models, outperforming larger proprietary ones in both accuracy and efficiency while ensuring data privacy through local fine-tuning and eliminating costly licenses. The dataset is curated by systematically augmenting variables from open-source HDL repositories to generate synthetic code snippets paired with corresponding assertions. Experimental results demonstrate that fine-tuned models like Deepseek Coder 6.7B and Llama 3.1 8B outperform GPT-4o, achieving up to 96.88% improvement over base models and 24.14% over GPT-4o on platforms including OpenTitan, CVA6, OpenPiton and Pulpissimo. VERT is available at https://github.com/AnandMenon12/VERT.

Figures (4)

• Figure 1: Dataset source distribution and composition.
• Figure 2: Generation of assertions from Case Statements.
• Figure 3: Generation of assertions from If statements.
• Figure 4: Comparison of GPT-4o and Fine-Tuned Model Performance.