HierSVA: A Data Synthesis Pipeline, Dataset, and Benchmark for LLM-Driven Hierarchical Hardware Formal Verification
- Year
- 2026
- Authors
- Maohua Nie, Jiang Zhu, Jingqun Zhang, Zhichen Zeng, Jiayi Wang, Sibo Zhang, Jialin Wang, C.-J. Richard Shi
- DOI
- 10.48550/arXiv.2606.13706
Related
Persistent Notes
In-text annotations
“BaseJump STL” Page 1
A standard library of sorts for SystemVerilog Page 1
“Applying HierSVA-B to twelve recent LLMs reveals three findings. First, the module-level compile rate is 67.1%; among generated assertions in evaluable runs, 82.1% prove non-vacuously, but the corresponding assertion sets detect only 70.2% of eligible injected faults and cover 36.2% of the formal core. Second, on 211 evaluable model–module entries in the deep subset, assertion sets flag buggy RTL with 0.87 recall, but 40% of predicted-buggy outcomes are false positives on correct RTL, limiting precision to 0.60. Third, agentic mode improves S1-style provability and strength metrics, but gains plateau and oscillate." Page 1
“1 Introduction” Page 1
“three places” Page 1
“limited sources of reference assertions” Page 1
Why do we need reference assertions? Can’t we just test the generated assertions with a Jasper? Are we checking for some sort of equivalence with the golden set? Page 1
“These limitations reflect the absence of a reusable pipeline for synthesizing reference assertions directly from RTL” Page 1
“Second, existing reference ∗Equal Contribution. Preprint. arXiv:2606.13706v1 [cs.AR] 9 Jun 2026 datasets are correspondingly small, flat, or templated, with cross-module dependencies excluded by construction [22]" Page 1
“Third, existing evaluations focus on syntax correctness and pass-or-fail metrics, leaving out vacuity, mutation coverage, and specification faithfulness [36, 24, 14]." Page 2
“First, the module-level compile rate is 67.1%; among generated assertions in evaluable runs, 82.1% prove non-vacuously. However, the corresponding assertion sets detect only 70.2% of eligible injected faults and cover only 36.2% of the formal core. This coverage gap becomes more pronounced with deeper hierarchy, as formal-core coverage drops from 75.5% at the bottom-most level to 5.9% at the second-to-top-most level. Second, on 211 evaluable model–module entries in the deep subset, LLM-generated assertion sets flag the buggy RTL with aggregate recall 0.87. However, 40% of predicted-buggy outcomes are false positives on the correct RTL, limiting aggregate precision to 0.60. Third, agentic mode partially improves the provability-versus-strength gap on S1-style metrics, but its gains plateau and fluctuate across iterations." Page 2
“2 Related Work” Page 2
“Benchmarks for LLM-generated assertions. A small number of benchmarks evaluate LLMs on SVA generation, and Table 1 positions them against HierSVA along the dimensions relevant to industrial deployment. AssertionBench [36] pairs OpenCores [33] designs with assertions mined using GoldMine [40] and HARM [17], and reports a pass/CEX/error trichotomy under JasperGold. FVEval [22] introduces three sub-benchmarks built from expert-written, synthetically generated, and template-generated test cases. Its Design2SVA subset uses parameterized pipeline templates and FSM templates rather than industrial multi-module codebases such as OpenTitan [25], thereby sidestepping the cross-module dependency context that HierSVA-B targets. AssertEval [24], AssertLLM [14], VERT [28], and CVDP [35] similarly focus on small open-source or synthetic designs, with evaluation protocols that either skip formal evaluation or fold quality into a single pass/fail number. More details and comparisons with this work are given in Appendix G." Page 2
Literature survey Page 3
![[assets/zimage-nieHierSVADataSynthesis2026-3-x99-y442.png]]
“3 HierSVA-SP: Dataset Synthesis Pipeline” Page 3
“3.1 Design Principles: Following Industry Practice” Page 3
“assume-guarantee composition (Section 3.3), mutation analysis through FTA, and formal core coverage analysis” Page 3
I dont know what these mean Page 3
“3.2 RTL Preprocessing” Page 3
“3.3 Hierarchical Composition with Submodule Contracts” Page 4
“3.4 Iterative Synthesis with Formal Feedback” Page 4
“4 HierSVA-DS: The Dataset” Page 5
“5 HierSVA-B: Benchmark Framework” Page 6
“6 Evaluation and Results Analysis” Page 7
“7 Conclusion and Discussion” Page 9
%% Import Date: 2026-07-11T14:08:20.980-04:00 %%