Research map / Large language models / Agents, code and math

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

NeurIPS 2026 · Large language models › Agents, code and math · approach: Execution-based code verification

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Introduces HierSVA, a synthesis pipeline (HierSVA-SP), a 342-module hierarchical SVA dataset from BaseJump STL (HierSVA-DS), and a six-axis benchmark (HierSVA-B) evaluating twelve LLMs on assertion generation under formal verification.

Problem

Existing LLM-for-SVA benchmarks rely on small, flat, or templated designs and report only syntax or pass/fail metrics, omitting vacuity, mutation coverage, spec faithfulness, and formal core coverage on hierarchical RTL.

Approach

An LLM-in-the-loop formal flow with deterministic RTL preprocessing and bottom-up assume-guarantee contracts synthesizes reference SVA for hierarchical modules, and a six-metric evaluation decomposes assertion quality beyond proof success.

Key results

• Module-level compile rate averages 67.1% across twelve LLMs; C2-P averages 82.1% but C4 is 70.2% and C5 formal core coverage is 36.2%.
• On 211 evaluable deep-subset entries, aggregate recall is 0.87 but precision is 0.60 because 40% of predicted-buggy outcomes are false positives on correct RTL.
• Agentic mode over five models on 40 modules raises C2-P by +21.1 pp, C4 by +10.6 pp, and C5 by +13.2 pp on average, but C4 and C5 oscillate across iterations.

Surprising findings

• Formal core coverage drops from 75.5% at the bottom-most hierarchy level to 5.9% at the second-to-top level.
• Iterative repair often deletes or weakens falsified properties, restoring provability while lowering mutation coverage.

Limitations

• The eligible-fault denominator for FTA is manually audited and not automated.
• Deep subset is small (28 module-bug pairs) and mostly LLM-synthesized bugs; reference assertions are LLM-generated rather than human-complete.
• Raw EDA tool logs cannot be released due to NDA restrictions; VC Formal is commercial.

Experimental setup

Datasets: BaseJump STL

Benchmarks: HierSVA-B HierSVA-DS

Metrics: syntax correctness (C1) assertion proof success rate (C2-P) vacuity rate (C2-V) specification faithfulness precision/recall (C3) mutation coverage (C4) formal core coverage (C5)

Baselines: AssertionBench FVEval AssertEval AssertLLM VERT CVDP

Builds on: AssertionBench FVEval AutoSVA

Closest papers by meaning

• VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification (NeurIPS 2025 · similarity 0.87)
• Lemur: Integrating Large Language Models in Automated Program Verification (ICLR 2024 · similarity 0.85)
• PCBSchemaGen: Reward-Guided LLM Code Synthesis for Printed Circuit Boards (PCB) Schematic Design with Structured Verification (NeurIPS 2026 · similarity 0.85)
• RvLLM: LLM Runtime Verification with Domain Knowledge (NeurIPS 2025 · similarity 0.84)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.84)
• Algorithm Selection for Word-Level Hardware Model Checking (Student Abstract) (AAAI 2025 · similarity 0.83)