VERT: A SystemVerilog Assertion Dataset to Improve Hardware Verification with LLMs

Authors: Anand Menon, Samit S Miftah, Shamik Kundu, Souvik Kundu, Amisha Srivastava, Arnab Raha, Gabriel Theodor Sonnenschein, Suvadeep Banerjee, Deepak Mathaikutty, Kanad Basu
Primary area: datasets and benchmarks
Keywords: Hardware Verification, Large Language Models, SystemVerilog

Abstract:
Hardware verification is a critical step in the modern System-on-Chip (SoC) design cycle, consuming approximately 70% of development time. SystemVerilog assertions are pivotal in the verification process, ensuring that designs function as intended. However, existing industrial practices rely on manual assertion generation, which becomes increasingly untenable as hardware systems become complex. Recent research has explored the potential of Large Language Models (LLMs) to automate the hardware verification process, reducing human intervention. Despite this, State-of-the-Art (SOTA) proprietary models, such as OpenAI's GPT-4o, have shown limitations in generating accurate assertions and require costly licenses and restricted usage. While smaller, open-source LLMs offer a more accessible option, they require fine-tuning to handle the complexities of the source code and generate accurate assertions. This highlights the need for a dataset that enables these models to achieve superior performance compared to SOTA LLMs. To this end, we present VERT, a dataset designed to improve the generation of SystemVerilog assertions using LLMs. Our dataset empowers researchers and hardware corporations to fine-tune smaller, open-source LLMs, surpassing larger proprietary models such as GPT-4 in accuracy and efficiency. Furthermore, VERT eliminates the need for expensive licenses and ensures data privacy through local fine-tuning, providing a scalable, cost-effective solution for automated hardware verification. To curate the dataset, we systematically compile and augment variables from open-source hardware description languages (HDL), generating conditions to create synthetic code snippets paired with corresponding assertions. We show that smaller, open-source LLMs, such as Deepseek Coder 6.7B and Llama 3.1 8B, when fine-tuned on VERT, outperform OpenAI's GPT-4o in assertion generation. The assertions generated by the fine-tuned models are evaluated on industry-standard platforms, including OpenTitan, CVA6, and Pulpissimo SoCs, demonstrating up to a 96.88% improvement in both functional and syntactical correctness compared to the base models and up to 24.14% when compared to GPT-4o. This demonstrates the prowess of VERT in enabling researchers to potentially reduce the overhead and human error associated with manual assertion generation, offering a scalable solution for industry-grade hardware designs. The dataset is available at https://anonymous.4open.science/r/VERT-4D6D/.

Decision: reject
Reviewer scores: 6, 5, 5

Reviews and discussion:
<thread>
creation date:
1730663660185

thread_type:
official_review

<thread_object>
creator: reviewer_lbj3

<content>
summary:
This paper proposes an open-source dataset named VERT to improve SystemVerilog assertion generation for large language models (LLMs). The authors identify existing gaps in the verification performance of off-the-shelf LLMs through examples. Their evaluation shows that VERT-fine-tuned LLMs achieve significant improvements in functional correctness and syntactical coverage.

strengths:
- Timely problem
- Good solution

weaknesses:
- Insufficient evaluation on verification effectiveness

questions:
Thank you for submitting to ICLR 2025. The research problem is both interesting and timely. The motivating examples are helpful for me to understand existing problems in the off-the-shelf models, and the experimental results show significant improvements.

The authors evaluated the effectiveness of their approach based on the total number of assertions and correctness in both syntax and functionality. However, these metrics do not reflect how important their assertions are. For example, one can generate a working assertion like 'assert True', but it has no impact on functional verification. It would be helpful if the authors could compare the importance of assertions, for example, using mutation tests: https://ieeexplore.ieee.org/abstract/document/10546742
</content>
</thread_object>

</thread>
<thread>
creation date:
1730676023143

thread_type:
official_review

<thread_object>
creator: reviewer_pihx

<content>
summary:
The article introduces a new dataset named VERT, specifically designed for generating SystemVerilog assertions to enhance the efficiency of the hardware verification process. Hardware verification is crucial in modern chip design, accounting for 70% of development time. However, the current reliance on manual assertion generation is inefficient and prone to errors. VERT systematically collects and augments variables from open-source hardware description languages, generating synthetic code snippets and corresponding assertions. This dataset aims to optimize the performance of smaller open-source large language models (such as DeepSeek Coder and Llama 3.1), enabling them to surpass proprietary models like GPT-4o. Additionally, the VERT dataset supports local fine-tuning, eliminating costly licensing fees and ensuring data privacy, thus providing a scalable and cost-effective solution for automated hardware verification.

strengths:
1. The VERT dataset provides a high-quality data source for generating SystemVerilog assertions, helping small open-source large language models generate accurate assertions in hardware verification.

2. With fine-tuning on the VERT dataset, smaller open-source models (such as DeepSeek Coder and Llama 3.1) can surpass proprietary models like GPT-4o in generating accurate assertions, demonstrating the feasibility and efficiency of open-source solutions in hardware verification.

3.  As an open-source dataset, VERT provides researchers and companies with the flexibility to expand it with additional hardware design scenarios as needed, laying a solid foundation for future research and applications in hardware verification.

weaknesses:
1. The authors compared the test results of GPT-4o and other models fine-tuned on VERT in Figure 4. Did the authors compare VERT with current benchmarks and remove data that could potentially contaminate the test set?

2. I would recommend that the authors consider submitting this article to a hardware-focused conference or journal, as the primary contribution of the work lies in the dataset generation process for VERT rather than in the field of artificial intelligence or deep learning. As such, I feel it somewhat diverges from the main objectives of ICLR:

> The International Conference on Learning Representations (ICLR) is the premier gathering of professionals dedicated to the advancement of the branch of **artificial intelligence** called representation learning, but generally referred to as **deep learning**.

questions:
See Weakness.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730682989555

thread_type:
official_review

<thread_object>
creator: reviewer_mh3q

<content>
summary:
This paper mainly proposes VERT, a dataset specially designed for improving the generation of SystemVerilog assertions using LLMs in hardware verification. The dataset is generated synthetically and contains a rich variety of conditions based on the cleaned variable list, allowing the model to learn complex hardware logic and generate accurate assertions without oversimplifying or omitting critical conditions. Experimental results show that small LLMs fine-tuned using the VERT dataset significantly outperform base models and GPT-4o in terms of syntax and functional correctness.

strengths:
1.	This paper is generally well-written and easy to follow, except some points. I can understand most statements easily. For some improvement suggestions, please see the weakness part below.
2.	The proposed dataset enables the small LLMs to significantly improve performance compared to the base and surpass GPT-4o without fine-tuning. And it also shows good effectiveness in real task scenarios.

weaknesses:
1.	Regarding the metrics of compilation success and simulation performance mentioned in the main contribution (4), I did not find any description of this part in the experimental section of the paper. 
2.	The paper’s experimental section is not comprehensive. It does not adequately validate the presented motivations and lacks some necessary ablation studies.
a)	Will the constructed dataset and the test dataset have the same modules, causing issues with training data leakage? 
b)	In section 4.1, regarding the intuition in dataset formulation, did the assertions generated by LLMs successfully address these issues?
c)	One important assumption made during the dataset construction is that the reuse of IPs would make it difficult for the model to differentiate between components. I think that an ablation study using a dataset constructed with an uncleaned variable list is needed to demonstrate this point.
3.	What is the coverage of the assertions generated by large language models?"
4.	I would like to know how the assertions generated by the fine-tuned LLMs compared to those designed by industrial experts in real-world task scenarios and the synthetic assertions through the method in section 4.3?

questions:
1.	Regarding the metrics of compilation success and simulation performance mentioned in the main contribution (4), I did not find any description of this part in the experimental section of the paper. 
2.	The paper’s experimental section is not comprehensive. It does not adequately validate the presented motivations and lacks some necessary ablation studies.
a)	Will the constructed dataset and the test dataset have the same modules, causing issues with training data leakage? 
b)	In section 4.1, regarding the intuition in dataset formulation, did the assertions generated by LLMs successfully address these issues?
c)	One important assumption made during the dataset construction is that the reuse of IPs would make it difficult for the model to differentiate between components. I think that an ablation study using a dataset constructed with an uncleaned variable list is needed to demonstrate this point.
3.	What is the coverage of the assertions generated by large language models?"
4.	I would like to know how the assertions generated by the fine-tuned LLMs compared to those designed by industrial experts in real-world task scenarios and the synthetic assertions through the method in section 4.3?
</content>
</thread_object>

</thread>
<thread>
creation date:
1732548206094

thread_type:
official_comment

<thread_object>
creator: area_chair_khng

<content>
comment:
Dear Reviewers,

This is a kind reminder that the dicussion phase will be ending soon on November 26th. Please read the author responses and engage in a constructive discussion with the authors.

Thank you for your time and cooperation.

Best,

Area Chair
</content>
</thread_object>

</thread>


Metareview:
metareview:
This paper introduces VERT, an open-source dataset designed for generating SystemVerilog assertions using large language models (LLMs) for hardware verification. The dataset is synthetically generated under various conditions, and experiments show that small LLMs fine-tuned on VERT outperform both base models and GPT-4 in terms of syntax and functional correctness. 

However, two of the three reviewers have recommended rejection, raising several concerns. First, the authors fail to compare VERT against existing datasets or control for potential test set contamination. Second, the paper's focus on hardware dataset generation seems misaligned with the scope of the ICLR venue, suggesting it might be better suited for hardware-related conferences. Finally, the evaluation metrics used are inadequate, as they do not adequately capture the significance of the generated assertions or provide a detailed analysis of the mutation testing results.

In conclusion, I do not recommend accepting this paper in its current form.