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

• URL: http://arxiv.org/abs/2606.13706v1
• Date: Tue, 09 Jun 2026 22:41:44 GMT
• Title: HierSVA: A Data Synthesis Pipeline, Dataset, and Benchmark for LLM-Driven Hierarchical Hardware Formal Verification
• Abstract summary: We present HierSVA, an integrated suite that combines a pipeline, dataset, and benchmark for formal verification.<n>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.<n>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.
• Score: 10.931713427869598
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: 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}.

Related papers

• SeGDeP: Semantic- and Geometric-Aware Decoupled Prompts for Reasoning Segmentation [51.46828526392219]
  Reasoning segmentation converts an implicit linguistic conclusion into a precise mask.<n>Existing MLLM-segmenter interfaces either use a special trigger or compress both signals into one context.<n>We present SeGDeP, an explicit what-where interface.
  arXiv  Detail & Related papers  (2026-09-08T15:11:32Z)
• Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations [0.0]
  Large language models (LLMs) are increasingly being explored for automated SystemVerilog Assertion (SVA) generation.<n>Most evaluations report correctness on a single syntactic representation of an input.<n>Such point accuracy does not reveal whether a model's correct output is stable when the same RTL behavior is written differently.
  arXiv  Detail & Related papers  (2026-09-04T18:41:58Z)
• EMRB: A Multi-Level Benchmark for Evaluating LLM Reasoning over Raw Electromagnetic Signals [18.190592357966]
  Large language models (LLMs) are increasingly used as code agents for scientific and engineering analysis, but their ability to analyze raw physical-layer measurements remains untested.<n>textbfEMRB (textbfElectrotextbfmagnetic textbfReasoning textbfBenchmark) evaluates whether LLMs can analyze raw I/Q data by writing and running code.
  arXiv  Detail & Related papers  (2026-08-25T05:33:24Z)
• A-SR: Self-Evolving Agentic LLMs for Symbolic Regression via Hierarchical Coordination [51.06539604709775]
  We propose A-SR, a self-evolving agentic framework that shifts the control unit from expression edits to role-conditioned evidence views.<n>A-SR coordinates formula discovery through routing among coordination protocols, an online evaluator-reward role policy, and state-routed process memory.
  arXiv  Detail & Related papers  (2026-08-05T14:01:10Z)
• Benchmarking LLMs for Verilog Design Flows [6.24010225101442]
  Large language models (LLMs) show promise in code generation, but their capabilities to produce correct, synthesizable hardware description language (HDL) code still remain to be properly benchmarked.<n>This paper presents a reproducible benchmarking platform that evaluates open-source LLMs on Verilog RTL generation.<n>The pipeline improved syntax validity from 0% to a 70.43% average and simulation pass rate to 51.8% across three open-source models.
  arXiv  Detail & Related papers  (2026-07-23T21:00:38Z)
• From Code to Prediction: Fine-Tuning LLMs for Neural Network Performance Classification in NNGPT [48.83701310501069]
  We present a classification task integrated into the NNGPT framework.<n>A fine-tuned LLM predicts which of two image classification datasets a given neural network architecture achieves higher accuracy on.<n>The results establish that LLMs can be fine-tuned to predict cross-dataset suitability from neural network code.
  arXiv  Detail & Related papers  (2026-05-05T12:30:19Z)
• Rewarding the Scientific Process: Process-Level Reward Modeling for Agentic Data Analysis [68.28714988482703]
  Process Reward Models (PRMs) have achieved remarkable success in augmenting the reasoning capabilities of Large Language Models (LLMs)<n>We present a study revealing that general-domain PRMs struggle to supervise data analysis agents.<n>We introduce DataPRM, a novel environment-aware generative process reward model.
  arXiv  Detail & Related papers  (2026-04-27T09:00:30Z)
• From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation [0.0]
  SystemVerilog Assertions (SVA) are essential for formal verification of digital hardware.<n>Recent studies have explored using large language models (LLMs) to automate SVA generation.<n>This paper presents ProofLoop, a tool-augmented ReAct agent that generates SVA from natural-language specifications.
  arXiv  Detail & Related papers  (2026-04-25T01:46:33Z)
• LLM-based Schema-Guided Extraction and Validation of Missing-Person Intelligence from Heterogeneous Data Sources [0.7734726150561088]
  Missing-person and child-safety investigations rely on heterogeneous case documents, including structured forms, bulletin-style posters, and narrative web profiles.<n>Variations in layout, terminology, and data quality impede rapid triage, large-scale analysis, and search-planning.<n>This paper introduces the Guardian Pack, an AI-driven parsing and normalization pipeline that transforms multi-source investigative documents into a unified, schema-compliant representation.
  arXiv  Detail & Related papers  (2026-04-08T01:35:56Z)
• QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis [41.09864485551356]
  We propose a data synthesis framework to tackle two challenges: the scarcity of high-quality real-world SVA corpora and the lack of reliable methods to determine NL-SVA semantic equivalence.<n>We train CodeV-SVA, a series of SVA generation models. Notably, CodeV-SVA achieves 75.8% on NL2SVA-Human and 84.0% on NL2SVA-Machine in Func.@1.
  arXiv  Detail & Related papers  (2026-03-15T06:25:09Z)
• ARIAL: An Agentic Framework for Document VQA with Precise Answer Localization [1.580774794371876]
  We present ARIAL, a framework that orchestrates specialized tools to achieve both precise answer extraction and reliable spatial grounding.<n>We evaluate ARIAL on four benchmarks (DocVQA, FUNSD, CORD, and SROIE) using both textual accuracy (ANLS) and spatial precision.<n>Our work demonstrates how agentic orchestration of specialized tools can simultaneously improve performance and interpretability.
  arXiv  Detail & Related papers  (2025-11-22T21:09:28Z)
• CLUE: Non-parametric Verification from Experience via Hidden-State Clustering [64.50919789875233]
  We show that correctness of a solution is encoded as a geometrically separable signature within the trajectory of hidden activations.<n>ClUE consistently outperforms LLM-as-a-judge baselines and matches or exceeds modern confidence-based methods in reranking candidates.
  arXiv  Detail & Related papers  (2025-10-02T02:14:33Z)
• Evaluating the Use of LLMs for Documentation to Code Traceability [3.076436880934678]
  Large Language Models can establish trace links between various software documentation and source code.<n>We create two novel datasets from two open-source projects (Unity Catalog and Crawl4AI)<n>Results show that the best-performing LLM achieves F1-scores of 79.4% and 80.4% across the two datasets.
  arXiv  Detail & Related papers  (2025-06-19T16:18:53Z)
• QiMeng-CodeV-R1: Reasoning-Enhanced Verilog Generation [51.393569044134445]
  Large language models (LLMs) trained via reinforcement learning with verifiable reward (RLVR) have achieved breakthroughs on tasks with explicit, automatable verification.<n> Extending RLVR to automatically generating hardware description languages (HDLs) like Verilog from natural-language (NL) specifications, however, poses three key challenges.<n>We introduce CodeV-R1, an RLVR framework for training Verilog generation LLMs.
  arXiv  Detail & Related papers  (2025-05-30T03:51:06Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.