SVAEval: An Evaluation Framework for LLM-based SVA Property Generators

Abstract

Assertion-based verification (ABV) uses SystemVerilog Assertions (SVA) to formally specify design behavior, but constructing high-quality SVA properties remains a labor-intensive and error-prone process. Recent advances in Large Language Models (LLMs) have enabled automated SVA generation from design specification documents; however, there are limitations in how the quality of the generated SVA properties, and thus the SVA generator, is evaluated. Existing automatic evaluation methods rely on formal tools – such as model checking and coverage analysis – to measure the correctness and completeness of the generated properties against a golden RTL implementation. However, it is difficult to obtain bug-free RTL designs, and even if they are available, the computed metrics do not accurately reflect the quality of generated properties against design specifications. We propose SVAEVAL, an automatic approach to evaluate SVA property generators, by directly evaluating the generated property sets without the need of golden RTL implementations. SVAEVAL considers two different scenarios: (1) If a human-expert-generated golden SVA property set is available (e.g., in a benchmark set), a formal framework is used to accurately evaluate the quality of the generated property set against the golden set. (2) Without a golden SVA property set, a hybrid formal and LLM-based framework is used to compare the quality of two generated property sets from different SVA generators. Experimental results demonstrate that SVAEVAL provides significantly more reliable evaluation than prior approaches, and offer new insights into the capabilities and limitations of various LLM-based SVA property generators.