Hardware functional verification relies on high-quality assertions to expose design bugs and establish confidence in Register Transfer Level (RTL) designs. Yet existing assertion mining methods still struggle to produce complete and reliable assertion sets: random or limited traces fail to cover hard-to-reach behaviors, and one-shot generation provides little feedback about what remains unverified or how the assertion set should be improved. As a result, critical design behaviors can remain uncovered even when many assertions are generated. We present NeuroAssertion, a coverage-driven assertion generation framework that combines formal trace generation, syntax-guided synthesis (SyGuS), and an agent-inspired refinement process within a unified framework. Our framework first converts hard-to-reach control-flow conditions into formal reachability objectives, uses model checking to generate behaviorally diverse traces, and mines initial assertions from these traces with SyGuS. It then performs targeted agent-inspired refinement under verification feedback: one LLM first proposes candidate assertions for uncovered regions, and if a candidate fails formal checking, a second LLM generates a repair grammar that guides constrained symbolic synthesis in a neuro-symbolic repair procedure. Experimental results show that this framework delivers around 2X more assertions and about 2X higher mutation coverage than traditional assertion mining methods.
Figures & tables
Figure 1. Coverage and assertion saturation with increasing random test cases on the b12 benchmark. Despite a 40 × increase in simulation effort, branch coverage plateaus at about 27% and the assertion count saturates at 35.
Figure 2. Overview of NeuroAssertion. S1 performs initial assertion generation, while S2 performs feedback-driven refinement. The final assertion set combines initial, directly verified, and repaired assertions.
Figure 3. RTL instrumentation for targeted reachability analysis. Inserted code is color-coded: auxiliary registers and branch markers are highlighted in green, while the generated SVA is highlighted in red.
Design
# RTL Lines
# Variables
Arb2
59
13
B12
738
26
I2C
1114
155
Ibex_controller
1101
233
Ibex_decoder
1156
141
Multdiv
353
59
Table 1. The statistics of benchmark designs in the experiment.
Figure 4. Overall experimental results compared with SMART. (a) shows the number of generated assertions, and (b) shows mutation coverage rate.
Figure 5. Ablation study of NeuroAssertion on representative benchmarks. (a) I2C, and (b) Pico.
Figure 6. Comparison with a direct LLM-based baseline. Subfigure (a) shows the number of generated assertions, and subfigure (b) shows mutation coverage.
Assertion-based verification (ABV) is a cornerstone of modern hardware design, yet manually translating design intent into formal SystemVerilog Assertions (SVAs) remains labor-intensive and error-prone. While Large Language Models (LLMs) show promise for automating this process, existing benchmarks remain limited by unrealistic task formulations, weak specification inputs, and oversimplified evaluation. To address these limitations, we introduce AssertLLM2, an open-source benchmark for realistic assertion generation in hardware verification. AssertLLM2 contains 83 real-world designs across 13 functional categories. For each design, the benchmark provides a structured design specification, a verified dependency-complete golden RTL, and systematically mutated buggy RTL variants. These support two practical settings: bug-prevention, where assertions are generated from specifications to guard against design errors, and bug-hunting, where assertions are generated to expose discrepancies between intended behavior and faulty implementations. To the best of our knowledge, AssertLLM2 is the first benchmark to explicitly use buggy RTL as input to evaluate bug-detection capability. AssertLLM2 further adopts a more rigorous evaluation framework spanning syntactic validity, formal provability, coverage, and mutation-based bug detection. Our benchmark enables a more realistic and extensive assessment of assertion generation and establishes rigorous baselines for state-of-the-art LLMs in practical hardware verification.
Yuchao Wu, Wenji Fang, Jing Wang +3
Hong Kong University of Science and Technology (HKUST)
SystemVerilog Assertions (SVAs) are crucial for hardware verification. Recent studies leverage general-purpose LLMs to translate natural language properties to SVAs (NL2SVA), but they perform poorly due to limited data. We propose a data synthesis framework to tackle two challenges: the scarcity of high-quality real-world SVA corpora and the lack of reliable methods to determine NL-SVA semantic equivalence. For the former, large-scale open-source RTLs are used to guide LLMs to generate real-world SVAs; for the latter, bidirectional translation serves as a data selection method. With the synthesized data, we train CodeV-SVA, a series of SVA generation models. Notably, CodeV-SVA-14B achieves 75.8% on NL2SVA-Human and 84.0% on NL2SVA-Machine in Func.@1, matching or exceeding advanced LLMs like GPT-5 and DeepSeek-R1.
Yutong Wu, Chenrui Cao, Pengwei Jin +6
SKL of Processors, Institute of Computing Technology, CAS Beijing, China · University of Chinese Academy of Sciences Beijing, China · University of Science and Technology of China Hefei, Anhui, China +1
Assertion-based Verification (ABV) is essential for ensuring that hardware designs conform to their intended specifications. However, existing automated assertion-generation approaches, such as LLM-based frameworks, often generate large numbers of redundant assertions, which significantly degrade simulation efficiency. To mitigate the simulation overhead caused by redundant assertions, this paper proposes Arcane, an efficient assertion reduction framework. It integrates a two-tier assertion clustering approach for accurate semantic classification of large assertion sets, and employs Monte Carlo Tree Search (MCTS) to explore optimal rule-application sequences for efficient assertion reduction. The experimental results on Assertionbench [20] show that Arcane achieves a reduction of up to 76.2% in the assertion count while fully preserving formal coverage and mutation-detection ability. Further simulation studies demonstrate a speedup of 2.6x to 6.1x speedup in simulation time. The proposed framework is released at https://anonymous.4open.science/r/Arcane1-0A6F/.
Hongqin Lyu, Yonghao Wang, Zhiteng Chao +2
State Key Lab of Processors, Institute of Computing Technology, CAS, Beijing, China · University of Chinese Academy of Sciences, Beijing, China