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

2. c. Ablation Study with Uncleaned Variable Names: We appreciate the suggestion and have conducted an ablation study with uncleaned variable names, presented in the Table below, to highlight the impact of cleaning variable names. The Table is split into two halves, containing the average percentage of Syntactically Correct Assertions and Functionally Correct Assertions across all the benchmarks outlined in Section 5.1. Columns 2 and 7 refer to the assertions generated by the base model. Columns 3 and 8 refer to assertions generated by a model fine-tuned on a dataset that contains syntactically incorrect variables (which refer to special characters not allowed in HDL languages); columns 4 and 9 refer to duplicate variables that may skew the model’s learning and introduce ambiguity, and columns 5 and 10 refer to inconsistent variables such as conflicting variable names. Finally, columns 6 and 11 refer to the cleaned variables we eventually use to build VERT. The results provided in the Table below demonstrate that failing to address syntactically incorrect variable names was the most critical, leading to lower performance in fine-tuned LLMs compared to even the base models. This is because the fine-tuned LLMs generate syntactically incorrect assertions stemming from erroneous variable names.

   Subsequently, LLMs fine-tuned with the cleaned variable list (VERT) performed up to 17.76% and 17.39% in syntactical and functional correctness, respectively, compared to the LLMs fine-tuned on a dataset that preserved duplicate variable names. This improvement is attributed to eliminating duplicates within the same assertion, which likely reduced ambiguity and enhanced the fine-tuned LLMs' ability to generate accurate results.

   Finally, addressing inconsistent variable names resulted in the smallest observed change, with the LLMs fine-tuned on the cleaned variable list increasing by up to 3.24% and 4.81%, in syntactical and functional correctness, respectively, compared to the LLMs fine-tuned on a dataset that maintained inconsistent variable names. This outcome is likely because such inconsistencies comprised a relatively minor portion of the overall variable list compared to the duplicates and syntactically incorrect variables. We have provided more details in Table 3 and Appendix A.6 of our manuscript.

3. Coverage Statistic: Complete Path Coverage (CPC) refers to covering all possible independent paths within an automaton. A path begins at the initial node, traverses through the graph's edges, and ends at a final node. While CPC provides a thorough examination of the system, it becomes infeasible for graphs containing cycles, as these can result in infinite path lengths [1]. In our approach, we use complete path coverage as our primary coverage metric. This ensures a comprehensive evaluation of the system's behavior by accounting for all potential paths. To validate our coverage, we employed both formal and simulation-based verification tools, including Cadence JasperGold and Xilinx Vivado. These tools allowed us to analyze the generated assertions and ensure that they cover all the functions defined within the system. By leveraging our method to extract properties from every possible conditional branch, we achieve up to 100% coverage. The information has been included and highlighted in Section 5.1 of the manuscript.

[1] J. Tong et al ., Defining and providing coverage for assertion-based dynamic verification. 2010 Journal of Electronic Testing 26

4. Comparison of LLMs fine-tuned on VERT with human experts: Human experts and LLMs fine-tuned on VERT generate assertions differently. Experts often create simpler, more readable assertions, reflecting a preference for human-friendly formats. LLMs, on the other hand, produce more standardized logical expressions. This difference highlights style preferences rather than superiority. Notably, despite these stylistic differences, LLMs fine-tuned on VERT achieve assertion generation performance comparable to that of human experts. We have provided examples in Text Box A.4 in Appendix A.5.2 of the manuscript. In Example 1, for instance, when verifying whether the bus_release_cnt signal has been reset, the LLM-generated assertion takes the form bus_release_cnt == '0', while the human expert expresses the same operation as !(|bus_release_cnt). The latter format, often favored by experts, is typically chosen for its ease of writing and brevity.

2. b. VERT Addressing Issues of existing LLM-based generated assertions: As outlined in the manuscript, currently, GPT-4o faces several key challenges, including (1) clock cycle and pre-condition capturing, (2) Miscapturing if Condition for else Branches, (3) Nested If-Else Conditions, and (4) handling long conditions. In this response, we demonstrate, using examples as follows, how LLMs trained on VERT address these issues. Relevant examples pertaining to this response have been included in Appendix A.5.1 of the manuscript.

   1. Clock Cycle Misinterpretations: We observe that LLMs often get confused between using the overlapping implication symbol ($|->$) and the non-overlapping symbol ($|=>$). To resolve clock cycle misinterpretation by LLMs, we standardized our format by using the overlapping implication symbol with a specified delay count and replacing the non-overlapping symbol. As shown in Text Box A.1 in Appendix A.5.1 of our manuscript, GPT-4o incorrectly uses the non-overlapping symbol, but both LLMs fine-tuned on VERT address this issue by correctly interpreting the clock cycle by using the overlapping implication symbol.
   2. Miscapturing if Condition for else Branches: LLMs often overlook the previous if/else if conditions when generating assertions for the subsequent else or else if branches in conditional statements. VERT addresses the common omission of conditions in the else/else-if branches of if-else statements by exposing the model to diverse conditional structures. As shown in Text Box A.2 in Appendix A.5.1 of our manuscript, GPT-4o, in its second assertion, misses that the second assertion should verify that monitor_enable is FALSE and monitor_enable_q is TRUE. However, both LLMs fine-tuned on VERT correctly identify these conditions and include them in the fourth generated assertion.
   3. Nested If-Else Conditions: LLMs often struggle with generating assertions for deeply nested if-else conditions (i.e., blocks nested beyond two levels), which are common in hardware design. To address the challenge of LLMs struggling with deeply nested if-else statements, we expanded VERT to include complex, multi-level conditional structures. As shown in Text Box A.2 in Appendix A.5.1 of our manuscript, GPT-4o incorrectly represents the logic of a nested block. Specifically, it ignores the if condition and creates an assertion using a ternary operator, where the inner if condition is used as the test, the assignment is the TRUE branch, and 1'b1 is the false branch. However, both LLMs fine-tuned on VERT to correctly identify the correct nested statement and their conditions.
   4. Handling Long Conditions: To address the challenge of generating accurate assertions for long and complex conditions, we expanded VERT to include a variety of cases where multiple conditions and operators must be evaluated simultaneously. As shown in Text Box A.3 in Appendix A.5.1 of our manuscript, the source code requires any one of six conditions to be met before raising the mr_err flag. However, the generated output by GPT- 4o creates three assertions for one flag change, each neglecting the other three conditions. This not only leads to incorrect assertion generation but also causes overhead in the number of assertions. However, both LLMs fine-tuned on VERT correctly generate a singular assertion that describes all the conditions and their relationships within the if-statement.

1. Metrics for Compilation Success and Simulation Performance: We thank the reviewer for raising the need for more clarity in our terminology. To clarify, Compilation Success refers to the compliance of the generated assertions with hardware description language standards, indicating they are Syntactically correct. In contrast, Simulation Performance assesses whether the assertions accurately reflect the intended hardware behavior, validating their expected functionality and confirming that they are Functionally correct.

   We acknowledge that this distinction was not sufficiently articulated in the original contributions of the manuscript. To address this, we have revised our writing to better align with the terminology used throughout the manuscript.  In specific, the updated contribution now reads: “Additionally, we evaluate the fine-tuned models using metrics such as syntactic and functional correctness, achieving up to 100% accuracy on modules from industry-standard SoCs, including OpenTitan, Pulpissimo and CVA6, thereby demonstrating the reliability and effectiveness of VERT in real-world scenarios.”

   Furthermore, the terms Syntactically correct and Functionally correct have been consistently applied in Table 1 and Section 5.2 of the manuscript to evaluate and report the performance of the fine-tuned models. This ensures alignment with the metrics defined throughout the manuscript, reinforcing the rigor and transparency of our evaluation methodology.

2. a. Training data leakage: We ensure that there is no overlap between the constructed dataset and the test benchmarks. Specifically, assertion examples from OpenTitan, CVA6, and Pulpissimo are not used in generating VERT. As detailed in Figure 1 of the manuscript, the constructed dataset (VERT) is synthesized from a curated and cleaned list of variables extracted from various open-source projects, including BOOM-core, Rocket-chip, and XiangShan. This figure provides a clear overview of the data sources and the systematic methodology employed, ensuring transparency and demonstrating the diversity and representativeness of the dataset for assertion generation. The test benchmark, on the other hand, consists of source code specifically derived from real-world System-on-Chip (SoC) designs, such as OpenTitan, CVA6, and Pulpissimo. These are distinct from the constructed dataset as they use actual hardware module code rather than synthetically generated code.

We thank the reviewer for their thoughtful and insightful comment regarding the evaluation metrics for our approach. Below, we address the concerns and provide clarifications:

The functional correctness of the generated assertions, as presented in Table 1 in the manuscript, was evaluated using mutation testing, consistent with the methodology outlined in [1]. This approach involved introducing intentional, small code modifications (mutants) that deviated from the expected assertion logic. By detecting these mutants, we demonstrated the effectiveness of the generated assertions in identifying logical inconsistencies and validating their utility. Unlike trivial or redundant assertions (e.g., "assert True"), these assertions were intricately aligned with the critical components of the hardware design, ensuring their relevance and impact.

Our findings revealed that the generated assertions achieved up to 100% functional correctness or ability to detect mutations across various benchmarks, underscoring their robustness and effectiveness. The same mutation testing methodology from [1] was also applied to verify the importance of the generated assertions, further affirming their significance. This comprehensive evaluation highlighted the non-redundant nature of the benchmarks and the potential of LLMs fine-tuned on VERT for hardware verification. Furthermore, the method ensured complete coverage of conditional branches and critical logic paths within the hardware design. The LLM-generated assertions were specifically crafted to validate every logical path, leaving no branch or condition unchecked, thereby reinforcing their role in achieving thorough hardware verification. We have incorporated this into our manuscript (highlighted in blue) in Section 5.1 and further elaborated in Appendix A.8.

[1] M. Iman et al., ARTmine: Automatic Association Rule Mining with Temporal Behavior for Hardware Verification: DATE 2024.

Dear Reviewer LBj3,

Thank you once again for your insightful comments and feedback on our paper. We have carefully considered your suggestions and prepared a detailed rebuttal in response. We sincerely appreciate reviewer Mh3q for reconsidering their score in light of our response. We would be happy to have your feedback as well and are grateful for any further thoughts you may have. We look forward to your thoughts on our rebuttal.

1. We thank the reviewer for raising this important point regarding comparison with other benchmarks. To the best of our knowledge, there are currently no publicly available benchmarks specifically designed for SystemVerilog assertion generation in hardware verification. Existing datasets and benchmarks focus primarily on Verilog code generation or hardware design, which makes direct comparisons with other datasets infeasible.

   Regarding potential data contamination, from our experiments, we observed that certain HDL components could negatively impact the generation of syntactically and functionally correct assertions. Notably, module instantiations and ifdef commands pose challenges for assertion generation. Specifically, the models used to evaluate VERT rarely generate assertions from module instantiations, leading to syntactically and functionally incorrect results.

   Moreover, these smaller models tend to misinterpret ifdef commands as conventional if-else statements. While this misclassification occurs infrequently, it reduces the percentage of correctly generated assertions. Assertions derived from these commands are often both syntactically incorrect—since ifdef commands do not adhere to standard if-else syntax and lack the necessary information for typical branching—and functionally incorrect, as they do not contribute meaningfully to functional branching. In contrast, GPT-4o appears to be unaffected by these HDL components in its assertion generation.

   Table 1 shows the impact of increasing contamination in design files on assertion generation. Column 1 lists the tested LLMs. Columns 2–4 ("Syntactically Correct (%)") display the percentage of syntactically valid assertions under no contaminants, an additional 10 contaminants, and an additional 20 contaminants. Columns 6–8 ("Functionally Correct (%)") show the percentage of assertions that are logically accurate and functionally aligned under the same contamination conditions. Here, “contamination” refers to the addition of ifdef commands and module instantiations. A contamination level lower than 10 was found to have a negligible impact on the results, while levels exceeding 20 were impractical due to exceeding the context size limitations of our models. The results show that as the level of contamination increases, the number of incorrectly generated assertions also rises. This results in a 3% drop in accuracy.  It should be noted that typically, in the hardware design, the number of ifdef commands is limited to at most five. Therefore, the scenarios used here to evaluate the contamination effect are unrealistic and for the purpose of studying the effect of contamination on the models. We have incorporated more detailed results into Appendix A.7 of our manuscript.

   Models		Syntactically Correct (%)			Functionally Correct (%)
   	No Contamination	+10 Contamination	+20 Contamination	No Contamination	+10 Contamination	+20 Contamination
   Llama 3.1	0.92	0.85	0.82	0.92	0.85	0.81
   DeepSeek	0.96	0.88	0.85	0.96	0.88	0.85

2. While the popular focus areas of the ICLR conference revolve around advancements in artificial intelligence and deep learning, the growing use of AI for automation in diverse domains, particularly in electronic design automation (EDA), is creating new and exciting application-centric tracks.

   We believe that while hardware-focused venues are a viable option, topics such as novel automation through dataset generation and LLM-driven EDA pipelines, including design verification, are highly relevant to ICLR. Similar emerging areas have been showcased at ICLR in the past, gaining traction and recognition. For instance, Hw-nas-bench: Hardware-aware neural architecture search benchmark [1], a hardware-centric benchmark paper, was presented during the rise of NAS, and Retrieval-Guided Reinforcement Learning for Boolean Circuit Minimization [2] was featured at ICLR 2024. These examples highlight how ICLR often welcomes emerging interdisciplinary communities under appropriate themes. We kindly request the reviewer to evaluate this draft under the relevant themes outlined in the ICLR CFP.

   1. Infrastructure, software libraries, hardware, etc.
   2. Applications to robotics, autonomy, planning
   3. Datasets and benchmarks

   Our work, which focuses on the novel automation of hardware design verification through dataset generation and LLMs, fits within these themes and represents an important and emerging topic in the field. We thank the reviewer for their feedback and hope these clarifications address their concerns.

[1] C. Li et al., HW-NAS-Bench: Hardware-Aware Neural Architecture Search Benchmark. ICLR 2024

[2] A. Chowdhury et al., Retrieval-Guided Reinforcement Learning for Boolean Circuit Minimization. ICLR 2024

Dear Reviewer piHx,

Thank you once again for your insightful comments and feedback on our paper. We have carefully considered your suggestions and prepared a detailed rebuttal in response. We sincerely appreciate reviewer Mh3q for reconsidering their score in light of our response. We would be happy to have your feedback as well and are grateful for any further thoughts you may have. We look forward to your thoughts on our rebuttal.