mlsanityData to 14 Oct 2026

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

arXiv 2606.13706 ↗First posted 9 Jun 2026cs.AR cs.AIcited by 0

Not on the map. Why?

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.

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

16 of 36 references.

References · 16

  1. 2018Datasheets for Datasetscited by 1,386
  2. 2025OpenAI GPT-5 System Cardcited by 989
  3. 2025Comprehensive Verilog Design Problems: A Next-Generation Benchmark Dataset for Evaluating Large Language Models and Agents on RTL Design and Verificationcited by 44
  4. 2024AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMscited by 31
  5. 2025OpenLLM-RTL: Open Dataset and Benchmark for LLM-Aided Design RTL Generationcited by 31
  6. 2023LLM4DV: Using Large Language Models for Hardware Test Stimuli Generationcited by 23
  7. 2024ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generationcited by 16
  8. 2024AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generationcited by 16
  9. 2025AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTLcited by 13
  10. 2021AutoSVA: Democratizing Formal Verification of RTL Module Interactionscited by 12
  11. 2024FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardwarecited by 10
  12. 2025Enhancing Large Language Models for Hardware Verification: A Novel SystemVerilog Assertion Datasetcited by 10
4 more
  1. 2025Spec2Assertion: Automatic Pre-RTL Assertion Generation using Large Language Models with Progressive Regularizationcited by 8
  2. 2025SANGAM: SystemVerilog Assertion Generation via Monte Carlo Tree Self-Refinecited by 2
  3. 2026Automated SVA Generation with LLMscited by 2
  4. 2025LASA: Enhancing SoC Security Verification with LLM-Aided Property Generationcited by 1

Built on by

Not cited yet.

Similar, not cited

Close in wording, no citation either way

  1. 2026A Survey on LLM-Integrated Hardware Design Verification
  2. 2025AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction
  3. 2026From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation
  4. 2026LLM-FSM: Scaling Large Language Models for Finite-State Reasoning in RTL Code Generation
  5. 2026Interpretable and Verifiable Hardware Generation with LLM-Driven Stepwise Refinement
  6. 2026Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair
  7. 2026Shift-Left High-Level Synthesis Verification via Knowledge-Augmented LLM Agent ↗
  8. 2026Structured Testbench Generation for LLM-Driven HDL Design and Verification-Oriented Data Curation