# HierSVA: A Data Synthesis Pipeline, Dataset, and Benchmark for LLM-Driven Hierarchical Hardware Formal Verification

arXiv: https://arxiv.org/abs/2606.13706 · HTML: https://mlsanity.com/paper/2606.13706/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 16 of its 36 references that are in the map.
- First posted on arXiv 9 Jun 2026.

## Builds on (most cited first, 16 of 16)

- [Datasheets for Datasets](https://mlsanity.com/paper/1803.09010/) (2018)
- [OpenAI GPT-5 System Card](https://mlsanity.com/paper/2601.03267/) (2025)
- [Comprehensive Verilog Design Problems: A Next-Generation Benchmark Dataset for Evaluating Large Language Models and Agents on RTL Design and Verification](https://mlsanity.com/paper/2506.14074/) (2025)
- [AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2402.00386/) (2024)
- [OpenLLM-RTL: Open Dataset and Benchmark for LLM-Aided Design RTL Generation](https://mlsanity.com/paper/2503.15112/) (2025)
- [LLM4DV: Using Large Language Models for Hardware Test Stimuli Generation](https://mlsanity.com/paper/2310.04535/) (2023)
- [ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation](https://mlsanity.com/paper/2402.00093/) (2024)
- [AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation](https://mlsanity.com/paper/2406.18627/) (2024)
- [AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL](https://mlsanity.com/paper/2503.19174/) (2025)
- [AutoSVA: Democratizing Formal Verification of RTL Module Interactions](https://mlsanity.com/paper/2104.04003/) (2021)
- [FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware](https://mlsanity.com/paper/2410.23299/) (2024)
- [Enhancing Large Language Models for Hardware Verification: A Novel SystemVerilog Assertion Dataset](https://mlsanity.com/paper/2503.08923/) (2025)
- [Spec2Assertion: Automatic Pre-RTL Assertion Generation using Large Language Models with Progressive Regularization](https://mlsanity.com/paper/2505.07995/) (2025)
- [SANGAM: SystemVerilog Assertion Generation via Monte Carlo Tree Self-Refine](https://mlsanity.com/paper/2506.13983/) (2025)
- [Automated SVA Generation with LLMs](https://mlsanity.com/paper/2604.11044/) (2026)
- [LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation](https://mlsanity.com/paper/2506.17865/) (2025)

## Abstract (arXiv)

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 coverage, and formal core coverage. 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. Codes and artifacts are available at hrefhttps://github.com/HierSVAAnon/HierSVACodeAndArtifactshttps://github.com/HierSVAAnon/HierSVACodeAndArtifacts. Dataset is available at hrefhttps://huggingface.co/datasets/AnonymousHierSVA/HierSVAhttps://huggingface.co/datasets/AnonymousHierSVA/HierSVA.