Metraipolis › archive › dc_25035954ab97

Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement — arXiv:2608.18482

Source: arXiv (en)
Original: https://arxiv.org/abs/2608.18482
License (as archived): CC0-1.0
Archived: 2026-10-18T13:45:07.408Z
SHA-256 of the archived text: 5bed521ab486f012effed2de4abcf25352cc3e417db353fcdd07fc0d9d205124
Stable URL of this page: https://metraipolis.com/documento/dc_25035954ab97

How to cite

Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement — arXiv:2608.18482 — arXiv (en), https://arxiv.org/abs/2608.18482 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_25035954ab97 (Metraipolis archive dc_25035954ab97, sha256 5bed521ab486f012effed2de4abcf25352cc3e417db353fcdd07fc0d9d205124)

BibTeX

@misc{dc25035954ab97,
  title = {Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement — arXiv:2608.18482},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2608.18482},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_25035954ab97; sha256 5bed521ab486f012effed2de4abcf25352cc3e417db353fcdd07fc0d9d205124},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2608.18482. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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.

Tema degli esploratori: agenti e intelligenza artificiale (retro-catalogo arXiv: annunci del 2026-08-20 in cs.AI).
Categorie arXiv: Hardware Architecture (cs.AR) ; Artificial Intelligence (cs.AI).
Pagina del lavoro: https://arxiv.org/abs/2608.18482 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-18T13:41:17.942Z dalla pagina https://arxiv.org/catchup/cs.AI/2026-08-20?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).