HierSVA: A Data Synthesis Pipeline, Dataset, and Benchmark for LLM-Driven Hierarchical Hardware Formal Verification
We present HierSVA, an integrated suite that combines a pipeline, dataset, and benchmark for LLM-driven hierarchical hardware formal verification. HierSVA-SP pairs an RTL preprocessing toolchain with an LLM-in-the-loop formal verification flow to produce reference SystemVerilog Assertions (SVA) on hierarchical RTL. Applying it to BaseJump STL yields HierSVA-DS, a dataset of 342 modules, with hierarchy metadata and depths 0--9, accompanied by a deep subset of 28 module-bug pairs with natural-language specifications and bug variants. HierSVA-B decomposes assertion quality into six metric axes: syntax correctness, assertion proof success rate, vacuity, specification faithfulness, mutation co...
| Authors | Maohua Nie, Jiang Zhu, Jingqun Zhang et al. |
|---|---|
| Primary category | cs.AR |
| Published | 9 June 2026 |
| Last updated at source | 9 June 2026 |
Popularity, last 2 days
0 now. Counts as reported by the source, snapshotted daily by Silytics.
Connected in the knowledge graph
- AnonymousHierSVA/HierSVADataset · cited by
Models and datasets referencing this paper
- AnonymousHierSVA/HierSVADataset
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 18 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.