# Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement

arXiv: https://arxiv.org/abs/2608.18482 · HTML: https://mlsanity.com/paper/2608.18482/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 24 references that are in the map.
- First posted on arXiv 19 Aug 2026.

## Builds on (most cited first, 4 of 4)

- [AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2411.14436/) (2024)
- [AutoSVA: Democratizing Formal Verification of RTL Module Interactions](https://mlsanity.com/paper/2104.04003/) (2021)
- [ChatSVA: Bridging SVA Generation for Hardware Verification via Task-Specific LLMs](https://mlsanity.com/paper/2604.02811/) (2026)
- [Iterative LLM-Based Assertion Generation Using Syntax-Semantic Representations for Functional Coverage-Guided Verification](https://mlsanity.com/paper/2602.15388/) (2026)

## Abstract (arXiv)

Hardware functional verification relies on high-quality assertions to expose design bugs and establish confidence in Register Transfer Level (RTL) designs. Yet existing assertion mining methods still struggle to produce complete and reliable assertion sets: random or limited traces fail to cover hard-to-reach behaviors, and one-shot generation provides little feedback about what remains unverified or how the assertion set should be improved. As a result, critical design behaviors can remain uncovered even when many assertions are generated. We present NeuroAssertion, a coverage-driven assertion generation framework that combines formal trace generation, syntax-guided synthesis (SyGuS), and an agent-inspired refinement process within a unified framework. Our framework first converts hard-to-reach control-flow conditions into formal reachability objectives, uses model checking to generate behaviorally diverse traces, and mines initial assertions from these traces with SyGuS. It then performs targeted agent-inspired refinement under verification feedback: one LLM first proposes candidate assertions for uncovered regions, and if a candidate fails formal checking, a second LLM generates a repair grammar that guides constrained symbolic synthesis in a neuro-symbolic repair procedure. Experimental results show that this framework delivers around 2X more assertions and about 2X higher mutation coverage than traditional assertion mining methods.