PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Zhiyuan Yan, Ziyue Zheng, Hongce Zhang

arXiv:2608.18482v1cs.ARcs.AI

TL;DR

Existing RTL assertion-mining methods struggle to reach hard-to-exercise behaviors and refine incomplete assertion sets. NeuroAssertion combines formal exploration, SyGuS mining, and feedback-driven neuro-symbolic refinement, producing around 2× more assertions and about 2× higher mutation coverage overall.

  • Problem

    RTL assertion mining remains limited by incomplete behavioral reachability and one-shot generation, while constructing high-quality assertions is labor-intensive and error-prone.

  • Method

    NeuroAssertion uses formal reachability exploration, SyGuS-based mining, and mutation-coverage-guided LLM proposal with grammar-constrained symbolic repair.

  • Results

    Around 2× more assertions and about 2× higher mutation coverage overall are achieved than with SMART and direct LLM generation across seven RTL benchmarks.

  • Takeaways & Limitations

    The results support coverage-driven refinement as a more effective basis for RTL assertion generation than purely SyGuS-based or one-shot workflows.

Abstract

from arXiv · show

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.

1 INTRODUCTION

NeuroAssertion frames RTL assertion mining as a coverage-driven refinement problem, addressing limited trace diversity and weak completeness feedback. It combines formal exploration, SyGuS mining, and mutation-guided LLM refinement, improving assertion quantity and mutation coverage on seven RTL benchmarks.

  • Motivation: High-quality SystemVerilog Assertions remain labor-intensive and error-prone, making assertion construction a persistent bottleneck in RTL verification flows.Assertion-based verification uses SVAs to express expected behaviors for simulation and formal property verification.
  • Limitations: Random or constrained-random traces can miss hard-to-reach RTL behaviors, while existing mining methods provide little feedback about uncovered behaviors or refinement needs.These limitations leave initial assertion sets incomplete and make assertion generation largely one-shot over observed traces.
  • Framework: NeuroAssertion converts hard-to-reach control-flow conditions into reachability objectives, uses formal exploration to generate diverse traces, and mines initial assertions with SyGuS.The framework performs formal exploration before syntax-guided assertion mining to expose behaviors that limited traces may miss.
  • Refinement: Mutation-coverage feedback targets uncovered obligations with LLM-generated candidate assertions and enables repair of failed candidates through an agent-inspired refinement loop.The framework combines LLM proposals with constrained symbolic repair guided by a generated repair grammar.
  • Evaluation: On seven RTL benchmarks, the full framework consistently improves assertion quantity and mutation coverage over SMART and direct LLM generation.This result supports the framework’s goal of moving beyond one-shot generation over limited observed behaviors.

2 PRELIMINARIES

This section introduces RTL designs and SVA target properties, then reviews SyGuS-based assertion mining and mutation coverage as the methodology’s two ingredients. SyGuS constrains assertion synthesis through grammars, while mutation coverage supplies feedback about insufficiently constrained behaviors.

  • The framework targets Verilog/SystemVerilog RTL designs whose properties are expressed as SystemVerilog Assertions (SVAs).
  • SyGuS-based assertion mining: SyGuS searches for formulas satisfying behavioral constraints while restricting candidates to those derivable from a context-free grammar.The grammar consists of nonterminals, terminals, a start symbol, and production rules.
  • SyGuS-based assertion mining: For RTL assertion mining, traces provide behavioral constraints and grammars define allowed operators, signal combinations, and temporal structures.Existing methods partition variables into smaller groups and synthesize assertions over local signal sets to keep search tractable.
  • Mutation-coverage feedback: Mutation coverage evaluates whether assertions distinguish perturbed RTL mutants from the original design through formal checking.Undistinguished mutants expose insufficiently constrained behaviors, which become uncovered obligations for refinement.

3 METHODOLOGY · 3.1 Challenges to Address

Existing assertion-mining workflows are limited by inadequate behavioral reachability and weak guidance for expanding assertion sets. Random or constrained-random traces can miss hard-to-reach RTL behaviors, while validation feedback rarely identifies uncovered behaviors as refinement targets.

  • 3.1.1 C1: Limited Behavioral Reachability.: Assertion-mining workflows commonly begin from random or constrained-random traces, making their behavioral basis dependent on exercised executions.This reachability dependence limits what downstream mining can discover.
  • 3.1.1 C1: Limited Behavioral Reachability.: 27% branch coverage and 35 assertions plateau despite a 40× increase in simulation effort on the b12 benchmark.The figure illustrates that simply increasing random test cases does not remove the reachability bottleneck.
  • 3.1.1 C1: Limited Behavioral Reachability.: Hard-to-reach RTL conditions may remain unexercised, so downstream assertion mining cannot recover the behaviors they represent.A condition such as a == 8’d222 on an 8-bit signal triggers with probability 1/256 per random test.
  • 3.1.1 C1: Limited Behavioral Reachability.: Increasing random simulations does not eliminate the bottleneck caused by behaviors that are difficult to reach.The cited example gives a per-test trigger probability of 1/256 for a == 8’d222 over an 8-bit signal.
  • 3.1.1 C1: Limited Behavioral Reachability.: After initial mining, existing workflows mainly check whether current assertions hold rather than identify which design behaviors remain uncovered.Their feedback therefore emphasizes assertion correctness over assertion-set completeness.
  • 3.1.1 C1: Limited Behavioral Reachability.: Existing workflows seldom elevate uncovered behaviors into explicit refinement targets for the next assertion-generation iteration.This leaves limited guidance for systematically expanding the assertion set.

3.2 Overview of NeuroAssertion

NeuroAssertion treats RTL assertion mining as a coverage-driven refinement loop rather than one-shot generation. It combines formal exploration, SyGuS-based mining, mutation-guided candidate proposals, and grammar-constrained symbolic repair.

  • Formal exploration: NeuroAssertion converts hard-to-reach control-flow conditions into reachability objectives and uses formal traces to strengthen initial SyGuS-based assertion mining.This formal exploration stage addresses incomplete coverage of difficult behaviors.
  • Neuro-symbolic refinement: The framework repairs failed candidate assertions through grammar-constrained symbolic synthesis, using mutation coverage to guide completeness feedback.This feedback-driven stage targets obligations left uncovered by the current assertion set.
  • Initial mining: RTL instrumentation and model checking generate traces that produce an initial assertion set A0 through strengthened SyGuS-based mining.The pipeline begins by generating behaviorally informative traces before refinement.
  • Neuro-symbolic refinement: Mutation analysis identifies uncovered obligations and drives a refinement cycle of neural proposal, formal checking, and symbolic repair.Candidates that pass checking are added directly, while failing candidates are repaired with grammar-constrained symbolic synthesis.

3.3 S1: Formal Exploration for Enhanced Assertion Mining

S1 enriches assertion mining by using formal reachability analysis to expose hard-to-reach RTL behaviors before refinement. It instruments branch coverage, converts targets into formal objectives, and mines assertions from resulting traces with iterative SyGuS and CEGAR.

  • Formal Exploration: S1 uses targeted formal reachability analysis to seek executions that random simulation is unlikely to expose, expanding the behavioral basis for assertion mining.The method addresses C1 before refinement begins by actively targeting hard-to-exercise behaviors.
  • Formal Exploration: For each RTL branch condition, S1 adds zero-initialized br_cov registers and update statements, then generates SVAs over coverage bits as formal objectives.Model-checker counterexample traces become test vectors exercising the target branches.
  • Assertion Mining: S1 runs SyGuS in an iterative CEGAR loop to synthesize an initial assertion set A0, using formal counterexamples to refine constraints and guide improved assertions.The symbolic miner remains unchanged; S1 supplies it with a richer set of observed behaviors.

3.4 S2: Coverage-Driven Neuro-Symbolic Refinement

S2 refines assertions by deriving uncovered mutation-coverage obligations and coupling LLM-guided candidate proposals with formal validation and grammar-constrained SyGuS repair. Valid candidates are added directly, while failed candidates guide localized symbolic repair under counterexample feedback.

  • Obligation-driven refinement: S2 derives uncovered obligations U0 from the initial assertion set A0 and uses them to drive neural proposal and grammar-constrained symbolic repair stages.The two stages are tightly coupled through mutation coverage.
  • Neural proposal stage: The first LLM proposes synthesis-compatible SystemVerilog assertions for uncovered regions, using RTL context and structured behavioral analysis rather than certifying correctness.Candidates include assertions, semantic descriptions, required signals, and verification metadata in structured JSON.
  • Formal validation: Each candidate is immediately checked formally: valid assertions enter the current set, whereas invalid ones proceed to repair because their implicated variables may preserve useful behavioral structure.The workflow avoids discarding failed candidates and restarting generation from scratch.
  • Neuro-symbolic repair: For failed candidates, the second LLM constructs a repair-oriented grammar over relevant signals, narrowing symbolic search without directly emitting the repaired assertion.The neural stage defines a semantically focused search space, while SyGuS performs the subsequent repair synthesis.
  • Neuro-symbolic repair: Repair continues with strengthened constraints after counterexamples; if the LLM-induced grammar is insufficient, SyGuS falls back to a default grammar over the same signal set.The resulting valid assertion is added to the refined set after symbolic synthesis and formal certification.

4 EXPERIMENT

NeuroAssertion is evaluated on seven RTL benchmarks against SMART and a direct GPT-5 baseline, with results showing higher assertion counts and mutation coverage. Ablations further attribute these gains to formal exploration and feedback-driven refinement.

  • Evaluation setup: The evaluation covers seven RTL benchmarks, including arbitration, ITC’99, I2C, three Ibex RISC-V components, and Pico-derived RTL.The benchmarks span varied design sizes and complexities.
  • Comparison with SMART: NeuroAssertion generally produces around twice as many assertions as SMART and delivers around a twofold overall mutation-coverage improvement.Coverage gains are especially pronounced for I2C, Ibex_decoder, and Pico: 10.51% to 36.21%, 6.45% to 32.31%, and 14.63% to 37.80%, respectively.
  • Ablation study: On I2C, the full method generates 244 assertions with 36.20% mutation coverage, versus 181 and 16.96% without feedback and 89 and 10.40% without formal exploration and feedback.On Pico, the full method generates 477 assertions with 37.80% coverage, compared with 427 assertions and 15.85% coverage for the reduced variant described.
  • Ablation study: Formal exploration increases useful candidate assertions, while refinement converts them into assertions that improve mutation coverage.Both components are important: removing feedback or removing both formal exploration and feedback substantially reduces performance on representative benchmarks.
  • Comparison with direct LLM baseline: NeuroAssertion outperforms GPT-5 w. planning on assertion quantity, including I2C (244 vs. 55), Ibex_controller (297 vs. 33), Pico (477 vs. 44), and Multdiv (44 vs. 0).The direct baseline uses task-specific prompts with RTL analysis and planning but lacks formal exploration and feedback-driven neuro-symbolic refinement.

5 RELATED WORKS

Recent machine-learning-based hardware-verification methods fall into specification-side approaches driven by requirements, waveform descriptions, or coverage targets, and RTL-oriented approaches.

  • Method Categories: Machine-learning-based verification methods are broadly grouped into specification-side and RTL-oriented methods.Specification-side examples include NL2SVA, ChatSVA, ChIRAAG, AssertLLM, CoverAssert, and LASP; the passage also identifies AutoSVA and an RTL-focused LLM-assisted flow as RTL-oriented examples.

6 CONCLUSION

NeuroAssertion is a coverage-driven RTL assertion-generation framework that integrates formal exploration, syntax-guided synthesis, and feedback-driven neuro-symbolic refinement. It uses instrumentation, model checking, and mutation-coverage feedback to guide targeted neural proposal and symbolic repair.

  • Framework: NeuroAssertion combines formal exploration, syntax-guided synthesis, and feedback-driven neuro-symbolic refinement for RTL assertion generation.The framework is presented as coverage-driven.
  • Formal exploration: RTL instrumentation and model checking expand the behavioral basis available for assertion mining.
  • Feedback-driven refinement: Mutation-coverage feedback identifies uncovered obligations that guide targeted neural proposal and symbolic repair.
Loading 2608.18482v1…