HierSVA-DS: A Hierarchical SystemVerilog Assertion Dataset for BasejumpSTL

HierSVA-DS is a dataset of LLM-generated, formally-verified SystemVerilog Assertions (SVAs) for 342 hardware modules drawn from the open-source BasejumpSTL library, spanning 8 functional groups (bsg_async, bsg_cache, bsg_dataflow, bsg_link, bsg_mem, bsg_misc, bsg_noc, bsg_tag) and hierarchy levels 0 through 9, with 11 additional legacy bsg_dmc modules included for completeness. Each module ships with its RTL source, a golden assertions.v file containing concurrent SVA properties (assertions, assumptions, and cover statements), the full per-iteration LLM generation and repair history, design metadata (clock and reset signals, reset polarity, combinational-vs-sequential classification), the parameter sweep under which proofs were closed, and the Synopsys VC Formal run scripts that reproduce them. Every property was mechanically checked end-to-end: assertions proven by FPV, covers shown reachable by COV, mutated faults detected under FTA mutation testing, and the absence of hidden assumptions confirmed by FC. Because modules are organized by depth in the design hierarchy, the dataset supports research on hierarchy-aware specification mining, compositional verification, curriculum-style training of assertion-generation models, and benchmarking of automated property-mining tools.

HierSVA-DS 是一个由大语言模型（LLM）生成、经形式化验证的SystemVerilog断言（SystemVerilog Assertions，SVAs）数据集，其样本取自开源BasejumpSTL库的342个硬件模块，覆盖8个功能分组（bsg_async、bsg_cache、bsg_dataflow、bsg_link、bsg_mem、bsg_misc、bsg_noc、bsg_tag）以及0至9级的设计层级，同时额外纳入11个经典bsg_dmc模块以提升数据集的完备性。每个模块均配套提供其RTL源代码、包含并发SVA属性（断言、假设与覆盖语句）的`assertions.v`文件、完整的逐轮LLM生成与修复历史记录、设计元数据（含时钟与复位信号、复位极性、组合式/时序式分类信息）、完成形式化验证所需的参数扫描配置，以及可复现验证流程的Synopsys VC Formal运行脚本。所有属性均经过全流程自动化校验：断言通过FPV得到形式化验证，覆盖语句经COV确认可被触发，FTA突变测试可检测到所有突变故障，且通过FC确认无隐藏假设存在。由于数据集按照设计层级深度对模块进行组织，其可支撑面向层级感知的规范挖掘、组合式验证、断言生成模型的课程式训练，以及自动化属性挖掘工具的基准测试等相关研究方向。