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 \href{https://github.com/HierSVAAnon/HierSVACodeAndArtifacts}{https://github.com/HierSVAAnon/HierSVACodeAndArtifacts}. Dataset is available at \href{https://huggingface.co/datasets/AnonymousHierSVA/HierSVA}{https://huggingface.co/datasets/AnonymousHierSVA/HierSVA}.

翻译：我们提出HierSVA，一个集流水线、数据集与基准测试于一体的综合套件，用于LLM驱动的层次化硬件形式化验证。HierSVA-SP将RTL预处理工具链与LLM-in-the-loop形式化验证流程相结合，为层次化RTL生成参考SystemVerilog Assertions（SVA）。将其应用于BaseJump STL后，得到包含342个模块及其层次元数据（深度0–9）的数据集HierSVA-DS，并附带28个模块-错误对的深度子集（含自然语言规格说明与错误变体）。HierSVA-B将断言质量分解为六个度量维度：语法正确性、断言证明成功率、空泛性、规格忠实性、变异覆盖率及形式化核心覆盖率。应用HierSVA-B对12种最新LLM进行评估，获得三项发现：首先，模块级编译成功率为67.1%；在可评估运行生成的断言中，82.1%通过了非空泛证明，但对应断言集仅检测出70.2%的注入故障，并覆盖36.2%的形式化核心。其次，在深度子集的211个可评估模型-模块条目中，断言集发现错误RTL的召回率为0.87，但40%的预测错误结果在正确RTL中为假阳性，导致精确率仅为0.60。第三，代理模式虽能改善S1风格的可证明性与强度指标，但增益存在平台期与波动。代码与工件详见\href{https://github.com/HierSVAAnon/HierSVACodeAndArtifacts}{https://github.com/HierSVAAnon/HierSVACodeAndArtifacts}。数据集详见\href{https://huggingface.co/datasets/AnonymousHierSVA/HierSVA}{https://huggingface.co/datasets/AnonymousHierSVA/HierSVA}。