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

HierSVA is introduced as a comprehensive suite for LLM-driven hierarchical hardware formal verification, comprising a data synthesis pipeline, dataset, and benchmark. The HierSVA-DS dataset includes 342 modules with hierarchy metadata and a subset of 28 module-bug pairs, while the HierSVA-B benchmark evaluates assertion quality across six metrics, revealing that generated assertions have a 67.1% compile rate and 82.1% non-vacuity proof success, but only detect 70.2% of faults. This framework is significant for practitioners as it provides a structured approach to enhance the reliability of hardware verification processes using LLMs, alongside access to relevant datasets and benchmarks for further research.