VERT: A SystemVerilog Assertion Dataset to Improve Hardware Verification with LLMs
Hardware Verification;Large Language Models;SystemVerilog
Yes
No ethics review needed.
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?
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.
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.
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?
Yes
No ethics review needed.
See Weakness.
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.
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.
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**.
Yes
No ethics review needed.
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
- Timely problem
- Good solution
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.
- Insufficient evaluation on verification effectiveness
This paper introduces VERT, a novel dataset that automates SystemVerilog assertion generation for hardware verification using Large Language Models.
@inproceedings{
anonymous2024vert,
title={{VERT}: A SystemVerilog Assertion Dataset to Improve Hardware Verification with {LLM}s},
author={Anonymous},
booktitle={Submitted to The Thirteenth International Conference on Learning Representations},
year={2024},
url={https://openreview.net/forum?id=rZmQ2z7MPA},
note={under review}
}
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/.
I certify that there is no URL (e.g., github page) that could be used to find authors’ identity.
I acknowledge that I and all co-authors of this work have read and commit to adhering to the ICLR Code of Ethics.
Hardware Verification Large Language Models SystemVerilog
I certify that there is no acknowledgement section in this submission for double blind review.
/pdf/244df6c4a7f5e81a3a31a6f1b0809745b20f051d.pdf
datasets and benchmarks
I understand the reciprocal reviewing requirement as described on https://iclr.cc/Conferences/2025/CallForPapers. If none of the authors are registered as a reviewer, it may result in a desk rejection at the discretion of the program chairs. To request an exception, please complete this form at https://forms.gle/Huojr6VjkFxiQsUp6.
I certify that this submission complies with the submission instructions as described on https://iclr.cc/Conferences/2025/AuthorGuide.
VERT: A SystemVerilog Assertion Dataset to Improve Hardware Verification with LLMs
ICLR 2025 Conference Submission
ICLR.cc/2025/Conference/Submission