PaperlayerView exact revision on arXiv

Source-linked AI summary

Agentic-IC3: Enabling Semantic Proof Search in IC3 Model Checking

Yu-Wei Fan, SooHyuk Cho, Aarti Gupta, Sharad Malik

arXiv:2609.27162v1cs.LOcs.AR

TL;DR

IC3’s generalization heuristics must identify useful lemmas, but bit-level representations can obscure high-level design relationships and higher-level approaches remain limited in exploiting design semantics. Agentic-IC3 brings an RTL-informed language-model agent into a persistent word-level IC3 proof session, where it proposes lemmas and can add observations or backtrack. It solves 10 of 14 benchmarks, including four cases unsolved by all three evaluated baselines.

  • Problem

    IC3 depends on useful generalization heuristics, yet bit-level representations make high-level design relationships difficult to exploit and word-level approaches remain limited in using design structure and semantics.

    Source: §1 · p. 2

  • Method

    Agentic-IC3 integrates an RTL-informed language-model agent into a persistent word-level IC3 backend to propose lemmas, add derived observations, and revise unproductive branches.

    Source: §1 · pp. 2–3

  • Results

    With a one-hour timeout per benchmark, Agentic-IC3 solves 10 of 14 cases, including four unsolved by rIC3, Pono-IC3Bits, and A-IC3.

    Source: §1 · p. 3

  • Takeaways & Limitations

    The ablation study reports fewer generalization interactions with batching and benefits from observations and backtracking on selected proof searches.

    Source: §8 · p. 18

    Current observations are limited to expressions over existing state, and useful relationships across execution stages may require persistent state; quantified lemmas and symbolic indexing are also future extensions.

    Source: Limitations and Extensions · p. 16

Abstract

from arXiv · show

IC3 is a state-of-the-art algorithm for hardware model checking that proves safety properties by incrementally constructing an inductive invariant consisting of a set of lemmas. Its effectiveness depends on generalization heuristics that identify useful lemmas and guide proof search. However, many leading IC3 hardware model checkers operate on lowered, bit-level representations, where high-level design relationships are difficult to exploit for generalization. Those operating at a higher level remain limited in exploiting high-level design structure and semantics. We present Agentic-IC3, built on Pono's word-level model-checking infrastructure, which integrates a language-model agent into IC3 to guide semantic proof search using register-transfer-level (RTL) design information. The framework exposes an agent-oriented interface to a persistent IC3 backend, allowing the agent to interact with an explicit, evolving proof state throughout verification. Across successive proof obligations, the agent relates intermediate proof states and solver feedback to the RTL and proposes high-level lemmas through both SAT and UNSAT generalization. Beyond generalization, the agent can introduce derived observation signals to express design relationships succinctly and obtain more informative feedback, and backtrack to revise proposals that lead to unproductive proof branches. The backend checks proposals before updating the proof state, preserving soundness and providing feedback for further reasoning. On a suite of 14 benchmarks spanning security information-flow verification and functional verification of communication protocols, processors, and functional units, Agentic-IC3 solves 10 cases within a one-hour timeout, including 4 unsolved by all three evaluated baselines: rIC3, Pono-IC3Bits, and A-IC3.

1 Introduction

IC3 generalization must capture design- and property-relevant relationships, but bit-level representations obscure some high-level structure and effective heuristics require substantial expertise. Agentic-IC3 uses an RTL-informed language-model agent within a persistent word-level IC3 session, solving 10 of 14 benchmarks, including four unsolved by all evaluated baselines.

1 Introduction

  • Useful generalization depends on design behavior and the property, making broadly transferable heuristics difficult to develop and requiring substantial expert effort.Existing approaches encode proof patterns through heuristics, grammars, and abstraction rules, whose effectiveness depends on their fit to target designs and properties.Source: §1 · p. 2
  • Bit-level lowering makes high-level design relationships difficult to identify, while word-level lemmas can express relationships such as equality or arithmetic constraints directly.The richer word-level representation also enlarges the search space, so heuristics may miss useful candidates.Source: §1 · p. 2
  • Agentic-IC3 integrates a language-model agent into Pono’s word-level model checker as a proof-search policy that uses RTL, properties, proof states, and solver feedback to propose lemmas.The agent examines signal relationships to explain an obligation’s unreachability.Source: §1 · p. 2
  • A persistent backend lets the agent use evolving proof context, introduce derived observation signals, and backtrack from unproductive branches; solver-checked updates preserve soundness and provide feedback.These actions let the agent shape both representation and direction of continuing proof search.Source: §1 · p. 3
  • With a one-hour timeout, Agentic-IC3 solves 10 of 14 benchmarks, including four unsolved by rIC3, Pono-IC3Bits, and A-IC3.The benchmarks span security information-flow and functional verification of communication protocols, processors, and functional units.Source: §1 · p. 3

2 Background

IC3 proves safety by constructing an inductive invariant from lemmas while refining a sequence of frames that overapproximate reachable states. Its backward proof search uses predecessor queries to expand obligations or block them with checked lemmas.

2 Background

  • An inductive invariant proves a safety property when it holds initially, is preserved by every transition, and implies the property.IC3 builds this invariant from lemmas that hold initially and are preserved by transitions.Source: §2 · p. 3
  • IC3 maintains frames F0 through Fk as overapproximations of states reachable within each transition depth, refining them by adding lemmas.A lemma in Fi need only hold within the first i transitions, not arbitrarily many transitions.Source: §2 · p. 3
  • A SAT predecessor query finds an earlier state, and SAT generalization expands it into a region whose states can reach the parent obligation.Repeated predecessor searches create a backward obligation tree; a branch reaching an initial state yields a counterexample.Source: §2 · pp. 3–4, Figure 1 · p. 4
  • An UNSAT predecessor query can permit blocking an obligation with a lemma ℓ whose negation excludes a larger region, after the lemma is checked and added to frames.Adding the checked lemma strengthens the frame approximations and blocks the obligation.Source: §2 · p. 4
  • Bit-level IC3 generalizes Boolean cubes and clauses by literal removal, whereas word-level IC3 can express multi-bit relationships such as equality directly.An equality between two n-bit registers requires 2n bit-level clauses in its bit-level representation.Source: §2 · p. 4

3 Motivating Example

The two-copy example contrasts bit-level generalization with an RTL-informed lemma that captures synchronization across execution phases. The example shows how the relationship between the controllers supports proving equal completion timing.

3 Motivating Example

  • The example checks whether two controllers with shared a and reset but assumption-constrained b inputs produce identical finish signals.The assertion tests whether permitted differences in b affect completion timing.Source: §3 · p. 5, Figure 2 · p. 5
  • Pono-IC3Bits greedily removes literals from q while preserving blocking conditions, yielding a bit-level blocking lemma.The passage identifies Pono-IC3Bits as the IC3Bits engine in Pono used as a conventional IC3 reference.Source: §3 · pp. 5–6
  • The bit-level lemma excludes DONE at frame 1, but DONE becomes reachable in later frames, so it does not capture the needed relationship.After one transition from initialization, the controller can only be in IDLE or WORK.Source: §3 · p. 6
  • The agent uses the RTL and input assumption to identify synchronized controller updates, capturing a relationship across execution phases that contributes to proving equal completion timing.Both counters load zero when a is zero and otherwise load equal b operands.Source: §3 · p. 6

4 Agentic-IC3 Framework

Agentic-IC3 couples an agent to a persistent, solver-checked IC3 proof state and uses RTL context to guide lemma proposals, observations, and revisions. Its framework batches SAT and UNSAT generalization and supports backtracking when recursive proof search becomes unproductive.

4 Agentic-IC3 Framework

  • The framework separates agent-guided proof-search decisions from IC3’s kernel, which checks proof updates.The agent uses RTL and accumulated context to propose lemmas, introduce observations, or revise proposals.Source: §4 · p. 6, Figure 3 · p. 7

4.1 Design and Agent Interface

  • The persistent interface retains frames, lemmas, obligations, and observations across requests, while presenting proof context through RTL names and expressions.Agent responses select Propose, Observe, or Backtrack; proposals use a parsed and type-checked subset of Verilog expressions compiled to bit-vector SMT formulas.Source: §4.1 · p. 7, Figure 3 · p. 7

4.2 Batch Generalization

  • Agentic-IC3 batches predecessor states for SAT generalization and checked blocking lemmas for UNSAT generalization, letting the agent reason over multiple examples alongside RTL and proof context.The agent can propose multiple lemmas, and the backend checks them before updating frames.Source: §4.1 · p. 7, §4.2 · pp. 8, 10
  • SAT proposals may exclude states beyond the current predecessor query, but bounded model checking rejects proposals with reachable violations before recursive blocking.If the BMC check passes, the backend recursively blocks the negated proposal and continues the IC3 search.Source: §4.2 · p. 9
  • For UNSAT generalization, a proposed lemma can replace batch lemmas it implies; the backend admits it only after initiation and relative-inductiveness checks pass.A failed check returns a counterexample for revision.Source: §4.2 · p. 10

4.3 Derived Observation Vocabulary

  • Named derived observations expose relationships among signals by adding their values to proof requests and reusing them across later obligations.For example, cnt1 + cnt2 is 8 in displayed states where active is asserted, although neither counter has a fixed value.Source: §4.3 · p. 10, Table 1 · p. 11

4.4 Backtracking and Proof Revision

  • The agent can backtrack from a recursive proof attempt and revise an earlier SAT proposal when later obligations reveal a more effective proof direction.Admitted lemmas remain in their validated frames and can prune subsequent search.Source: §4.4 · p. 11

5 Evaluation

Across 14 hardware-verification benchmarks, Agentic-IC3 solves cases beyond the evaluated baselines. Ablations and proof trajectories show how batching, observations, and backtracking shape its search, alongside limitations that motivate richer lemma and observation mechanisms.

5.1 Comparison with IC3 Baselines

  • Agentic-IC3 solves 10 of 14 benchmarks within one hour, including four cases unsolved by rIC3, Pono-IC3Bits, and A-IC3.It solves every case solved by rIC3 or A-IC3, which each solve five; Pono-IC3Bits times out on all 14.Source: §5.1 · p. 12, Table 2 · p. 13
  • Across ten completed runs, agent-response waits account for 87% of aggregate runtime; on multiplier, Agentic-IC3 takes 21.23 seconds versus approximately three seconds for rIC3 and A-IC3.The authors suggest reducing agent-response latency as a potential route to better end-to-end performance and propose fine-tuning smaller models.Source: §5.1 · pp. 12–13

5.2 Ablation Study of Individual Mechanisms

  • Batch generalization reduces total generalizations from 515 to 137, or 73%, while both configurations solve all ten benchmarks.Batching reduces runtime on nine benchmarks, with speedups of 3.3× on fp_divider and 2.6× on fp_adder.Source: §5.2 · p. 13
  • With observations, the full system solves one more benchmark; on gulwani_fig1a_2_ebmc it completes in 175.73 seconds, while the no-observations run times out after 41 generalizations.On cache and fifo_vis, the full system also uses half as many generalizations; the no-observations run is faster on bsg_link, possibly due to run variation.Source: §5.2 · p. 14
  • Backtracking reduces generalizations from 67 to 23 on fp_adder and from 43 to 11 on nerv_causal, with runtime speedups of 2.3× and 10.5×, respectively.Both configurations solve all ten benchmarks; the fp_adder trajectory shows the agent replacing an early equality proposal with relationships restricted to relevant control states.Source: §5.2 · p. 14

Agent Decisions

  • For multiplier completion, the agent proposes operand and busy-flag relationships that capture when both instances detect zero simultaneously, and the backend admits them to complete the proof.In the trajectory, the agent backtracks from equality required before register updates and replaces it with lemmas conditioned on control state.Source: Agent Decisions · pp. 15–16
  • For fifo_vis, an occupancy observation links ring-buffer occupancy to the shift-register tail representation, enabling the backend to admit a lemma relating them.The four-bit observation is rb.head − rb.tail modulo 16; the lemma handles nonempty, initialization, and empty cases.Source: Agent Decisions · p. 15

Limitations and Extensions

  • The current lemma language requires explicit indexed cases for some uniform relationships, while state-only observations cannot retain values across execution stages.Quantified or symbolic-index lemmas would require backend support and do not guarantee faster verification; stateful observations would require initialization and update rules.Source: Limitations and Extensions · pp. 16–17

6 Discussion

The discussion presents Agentic-IC3 as a common interface for combining proof-guidance actions according to evolving proof context. It also identifies trace analysis, specialized policy learning, and broader or more selective agent intervention as directions for investigation.

Combining established forms of proof guidance

  • Agentic-IC3 combines synthesis-based lemma generation, proof-vocabulary extensions [11], and global learned-lemma guidance [22] through one context-aware action interface.The backend maintains proof conditions while the agent selects and applies actions.Source: §6 · p. 17

Understanding and debugging proof search

  • Interaction traces connect proposed relationships and solver feedback to RTL, helping reveal missing observations, repeated proposals, and opportunities to refine the interface.A floating-point-adder trajectory shows operand equality and decoded-field equality becoming relevant at different control states.Source: §6 · p. 17

Learning specialized proof-search policies

  • Recorded traces could train smaller models for lemma generation and action selection, while agent guidance could extend to interpolation-based model checking.Useful training signals would account for proof progress and search cost, not just lemma validity.Source: §6 · p. 17

Alternative integration and global reflection

  • The discussion proposes triggering agent intervention after repeated obligations or limited frame progress, and periodically reviewing broader proof progress.The benefits of these approaches would need evaluation against added reasoning and coordination costs.Source: §6 · p. 18

7 Related Work

Agentic-IC3 is positioned as an RTL hardware-verification interaction framework that extends agent guidance beyond lemma generation. It can also serve as a verification backend for helper-invariant generation frameworks.

Related work

  • IC3Syn integrates LLM-generated blocking clauses into an IC3 controller for distributed protocols [2]; Agentic-IC3 adds RTL interaction, observations, and proof-obligation revision.The framework operates within a persistent IC3 session and extends guidance beyond lemma generation.Source: §7 · p. 18
  • Agentic-IC3 could serve as a verification backend for Large Lemma Miners and CIll, which generate helper invariants from design information and verification feedback [14] [17].Source: §7 · p. 18

8 Conclusion

The conclusion summarizes Agentic-IC3 as a persistent, solver-checked IC3 framework in which an LLM agent guides proof search using RTL and solver feedback. It reports benchmark results and identifies future evaluation and extension directions.

8 Conclusion

  • Agentic-IC3 solves 10 of 14 benchmarks, including four unsolved by all three baselines.Source: §8 · p. 18
  • The ablation study reports fewer generalization interactions with batching and benefits from observations and backtracking on selected proof searches.Source: §8 · p. 18
  • Future work will examine run-to-run variability, additional agent actions, and extensions to other model-checking algorithms.Source: §8 · p. 18
Loading 2609.27162v1…