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

• URL: http://arxiv.org/abs/2608.18482v1
• Date: Wed, 19 Aug 2026 03:14:14 GMT
• Title: Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement
• Abstract summary: NeuroAssertion is a coverage-driven assertion generation framework.<n>It combines formal trace generation, syntax-guided synthesis, and agent-inspired refinement.<n>It delivers around 2X more assertions and about 2X higher mutation coverage than traditional assertion mining methods.
• Score: 3.5085139194562456
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs [10.916179875278326]
  We introduce SKILLFORGE, a framework that decomposes formal code synthesis into a library of atomic, reusable skills.<n>A verification-driven harness orchestrates these skills.<n>On a curated benchmark of natural language to Dafny specification pairs, SKILLFORGE substantially outperforms both state-of-the-art agentic approaches.
  arXiv  Detail & Related papers  (2026-08-30T15:15:00Z)
• Execution-Anchored Hallucination Calibration Reranking for Verilog Code Generation [19.257000641887828]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, yet their performance degrades significantly on low-resource languages.<n>We propose EAHC, an Execution-Anchored Hallucination reranking framework that anchors reasoning judgments to execution behavior.
  arXiv  Detail & Related papers  (2026-08-24T08:11:43Z)
• Agent-Based Test Assertion Generation via Diverse Perspective Aggregation [13.443058740546164]
  AssertMate is a novel agent-based assertion generation framework.<n>It enhances the quality and reliability of large language models (LLMs) generated assertions.<n>It significantly outperforms state-of-the-art techniques in compilation success and pass rates.
  arXiv  Detail & Related papers  (2026-08-06T09:51:43Z)
• Escaping Confidence Trap: Evolutionary Decoding for Mathematical Reasoning in Diffusion LLMs [69.52853771994451]
  We analyze the decoding trajectories of LLaDA 2.0 and identify a recurring diffusion confidence trap.<n>We propose Evolutionary Decoding, a training-free test-time scaling framework that views diffusion decoding as an evolutionary process.
  arXiv  Detail & Related papers  (2026-08-01T11:48:25Z)
• AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications [7.797719198801956]
  We introduce AssertLLM2, an open-source benchmark for realistic assertion generation in hardware verification.<n>AssertLLM2 contains 83 real-world designs across 13 functional categories.<n>For each design, the benchmark provides a structured design specification, a verified dependency-complete golden RTL, and systematically mutated buggy RTL variants.
  arXiv  Detail & Related papers  (2026-05-26T10:49:25Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• AgentV-RL: Scaling Reward Modeling with Agentic Verifier [63.55502685076245]
  Verifiers have been demonstrated to enhance LLM reasoning via test-time scaling (TTS)<n>We propose Agentic Verifier, a framework that transforms reward modeling into a multi-turn, tool-augmented deliberative process.<n>We show that Agentic Verifier yields consistent performance gains under both parallel and sequential TTS.
  arXiv  Detail & Related papers  (2026-04-17T12:27:36Z)
• Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
  silicon-grade correctness remains bottlenecked by: (i) limited test coverage and reliability of simulation-centric evaluation, (ii) regressions and repair hallucinations, and (iii) semantic drift as intent is reinterpreted across agent handoffs.<n>We propose Veri-Sure, a multi-agent framework that establishes a design contract to align agents' intent and uses a patching mechanism guided by static dependency slicing to perform precise, localized repairs.
  arXiv  Detail & Related papers  (2026-01-27T16:10:23Z)
• Metacognitive Self-Correction for Multi-Agent System via Prototype-Guided Next-Execution Reconstruction [58.51530390018909]
  Large Language Model based multi-agent systems excel at collaborative problem solving but remain brittle to cascading errors.<n>We present MASC, a metacognitive framework that endows MAS with real-time, unsupervised, step-level error detection and self-correction.
  arXiv  Detail & Related papers  (2025-10-16T05:35:37Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• Are LLMs Ready for Practical Adoption for Assertion Generation? [6.3585378855805725]
  The quality of hardware verification, i.e., detection and diagnosis of corner-case design bugs, is critically dependent on the quality of the assertions.<n>With the onset of generative AI such as Transformers and Large-Language Models (LLMs), there has been a renewed interest in developing novel, effective, and scalable techniques of generating functional and security assertions.
  arXiv  Detail & Related papers  (2025-02-28T01:34:45Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  Large language models (LLMs) are increasingly integrated into real-world personalized applications.<n>The valuable and often proprietary nature of the knowledge bases used in RAG introduces the risk of unauthorized usage by adversaries.<n>Existing methods that can be generalized as watermarking techniques to protect these knowledge bases typically involve poisoning or backdoor attacks.<n>We propose name for harmless' copyright protection of knowledge bases.
  arXiv  Detail & Related papers  (2025-02-10T09:15:56Z)

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.