PaperlayerView exact revision on arXiv

Source-linked AI summary

Enhancing Word-Level Property Directed Reachability with LLM-Driven Semantic Guidance

Guangyu Hu, Mingkai Miao, Zhiyuan Yan, Xiaofeng Zhou, Wei Zhang, Hongce Zhang

arXiv:2609.30131v1cs.AR

TL;DR

Bit-level PDR can struggle when bit-blasting obscures word-level relations needed for datapath proofs. LLM4PDR proposes verifier-checked semantic helpers for word-level PDR; across benchmark suites, its modes show complementary benefits in different design classes.

  • Problem

    Bit-blasting can obscure compact datapath relations, while discovering proof-relevant word-level relations remains a bottleneck for word-level PDR.

    Source: §I · p. 1, D. Clause and Literal Explosion in PDR · p. 4

  • Method

    LLM4PDR uses LLM-generated predicates, clauses, and assertions as semantic helpers, with the verifier checking artifacts before they affect proof search.

    Source: §I · p. 2

  • Results

    Across suites, assertion guidance is strongest on arithmetic, clause guidance on deep HLS pipelines, and predicate guidance on open-source control-plus-datapath designs; LLM2Predicate reduces intersymbol_conv from 613.64 s to 3.06 s.

    Source: F. Ablation: IC3bits vs. IC3ng · p. 12, §VI · p. 13

  • Takeaways & Limitations

    The results indicate that verifier-checked LLM-generated semantic hints can be a practical and sound complement to conventional PDR generalization.

    Source: §VI · p. 13

Abstract

from arXiv · show

Property Directed Reachability (PDR) is a prominent algorithm for hardware formal verification. However, bit-level PDR often struggles with datapath-heavy designs because bit-blasting obscures high-level semantics. While word-level PDR addresses this by reasoning over bit-vector and array theories, its performance remains bottlenecked by discovering proof-relevant word-level relations. We propose LLM4PDR, a framework leveraging Large Language Models (LLMs) to guide word-level PDR search through three mechanisms: (1) Predicate Generation, extracting state relationships as candidate predicates during inductive generalization; (2) Clause Generation, producing candidate frame lemmas to accelerate convergence after formal validation; and (3) Assertion Generation, synthesizing helper assertions that strengthen the target property under counterexample-guided refinement. We implement LLM4PDR in the Pono model checker and evaluate it on arithmetic micro-benchmarks, HLS-generated pipelines, open-source RTL components, and hardware model checking competition (HWMCC) instances. Results show LLM-generated guidance improves both solved instances and runtime on datapath-heavy and control-plus-datapath designs. The strongest configuration solves 28 of 33 arithmetic benchmarks, compared to 13 for vanilla Pono and 11 for AVR. On HLS pipelines and open-source RTL, different modes provide complementary speedups: clause guidance is effective for deep pipelines and predicate guidance for bus and memory-controller designs. On HWMCC benchmarks, benefits are instance-dependent, demonstrating notable speedups and timeout avoidance on hard cases. These results suggest that LLM-generated, verifier-checked semantic hints can serve as a practical complement to conventional word-level PDR.

I. INTRODUCTION

Bit-blasting can obscure datapath relations that word-level PDR needs to prove, while low-level solver feedback may not reveal those relations. LLM4PDR supplies semantic hints at three points in the proof workflow, with the verifier checking every artifact.

I. INTRODUCTION

  • Bit-blasting datapath structures can obscure compact arithmetic and relational facts, making them harder for bit-level PDR to use.Word-level PDR represents such facts directly, but proof-relevant relations can remain difficult to discover.Source: §I · p. 1
  • Solver feedback may expose local value pairs rather than a needed higher-level relation, leading PDR to learn many weak clauses.The example given is a fixed offset between counters.Source: §I · pp. 1–2
  • LLM4PDR adds helper predicates during inductive generalization, helper clauses as candidate frame lemmas, and helper assertions to strengthen the target property.Assertions may be removed when counterexamples show they are invalid.Source: §I · p. 2
  • LLM4PDR guides word-level PDR with LLM-generated semantic hints while leaving proof decisions to the verifier.The model checker parses, type-checks, validates, and either uses or discards the generated artifacts.Source: §I · p. 2
  • The helper interface uses restricted SMT-LIB2, and the verifier parses, type-checks, validates, and refines generated artifacts before they affect proof search.The LLM is a hint generator, not a proof oracle.Source: §I · p. 2
  • LLM4PDR is implemented in Pono and evaluated on arithmetic, HLS-generated, open-source RTL, and HWMCC benchmarks.The reported benefits include more solved arithmetic cases and speedups or timeout avoidance on several hard word-level instances.Source: §I · p. 2

II. PRELIMINARIES AND PROBLEM FORMULATION

The preliminaries define the transition-system and frame concepts used by PDR, then describe how proof obligations are blocked and generalized. MIC uses solver checks and literal dropping, but its generalization lacks semantic understanding of literal roles.

A. Symbolic Transition Systems

  • A transition system is specified by state variables, inputs, an initial-state formula, and a transition relation; safety asks whether every reachable state satisfies the property.Priming a formula means replacing each state variable with its next-state version.Source: A. Symbolic Transition Systems · p. 2

B. The PDR Algorithm

  • PDR incrementally builds over-approximating frames whose clauses satisfy monotonicity, consecution, and safety conditions.A fixpoint between consecutive frames provides an inductive invariant proving the property.Source: B. The PDR Algorithm · pp. 2–3
  • PDR alternates between blocking counterexample-to-induction states and propagating clauses; reaching an initial state during backward blocking establishes a violation.A CTI is a state admitted by the current over-approximation that violates the target property.Source: B. The PDR Algorithm · pp. 2–3

C. Proof Obligation Handling and Inductive Generalization

  • When a CTI has no predecessor in the prior frame, its negation is inductive relative to that frame; otherwise, blocking recursively handles its predecessor.A successfully generalized clause is added to frames to block the state.Source: C. Proof Obligation Handling and… · p. 3
  • MIC tries to strengthen the negation of a state by dropping literals while retaining inductiveness relative to the previous frame.A stronger clause blocks a larger set of unreachable states and can accelerate convergence.Source: C. Proof Obligation Handling and… · p. 3
  • DOWN uses an unsatisfiable core to drop unnecessary literals, while a satisfiable check yields a predecessor used to further generalize the cube.The procedure also checks initiation and retains literals when required.Source: C. Proof Obligation Handling and… · p. 3
  • MIC's literal-dropping order relies on a fixed order or solver core extraction, without semantic understanding of the literals' roles in the design.This can produce local bit-level patterns and many clauses instead of a compact word-level fact.Source: C. Proof Obligation Handling and… · pp. 3–4

D. Clause and Literal Explosion in PDR

Bit-level PDR can incur clause and literal explosion when a proof depends on a compact word-level relation. LLM4PDR proposes such relations as helpers, while verifier checks determine whether they enter the proof search.

D. Clause and Literal Explosion in PDR

  • A word-level relation can become many bit-level clauses, each with many literals, producing clause and literal explosion that enlarges proofs and slows SAT queries.At word level, relations such as a = b+c are single atoms, but bit-blasting disperses them over variable bit slices.Source: D. Clause and Literal Explosion in PDR · p. 4
  • Existing approaches use auxiliary definitions from fixed patterns or word-level terms and predicates from hand-crafted rules, which may miss design-specific relations.PdrER needed more than 65,000 invariant clauses on one buffer-allocation benchmark without auxiliary definitions.Source: D. Clause and Literal Explosion in PDR · p. 4
  • LLM4PDR proposes predicates, clauses, or assertions from RTL or BTOR2 input, but the verifier checks each artifact before it can affect soundness.Predicates are candidate atoms, clauses must pass frame-consistency checks, and assertions are filtered using counterexamples.Source: D. Clause and Literal Explosion in PDR · p. 4
  • Figure 2 is captioned as an example of a property that is hard for existing SAT-based model-checking algorithms.The caption identifies the figure's scope but gives no comparative outcome.Source: Figure 2 · p. 4

III. MOTIVATION

A word-level invariant can be obvious from the hardware updates yet difficult for existing engines to discover from low-level encodings. LLM4PDR uses static design information to propose verifier-checked helpers for PDR.

III. MOTIVATION

  • The example’s invariant rai − ra = rbi − rb follows from identical counter guards, but bit-level subtraction expands into 16-bit carry propagation.The relationship holds across reachable states; once proposed, the verifier can check it with initiation and consecution queries.Source: §III · pp. 4–5
  • Berkeley-ABC, rIC3, AVR, and PdrER all exceed the one-hour timeout for widths 16–20 on the motivating example.The table covers model-checker results for widths 16 to 20; the text reports a 3600-second limit for every tested width.Source: Table I · p. 4, §III · pp. 4–5
  • LLM4PDR proposes predicates, clauses, or assertions from static RTL or BTOR2, unlike DreamMiner, which learns property augmentations from simulation traces.The LLM is a semantic guide rather than a trusted proof oracle; the verifier checks generated candidates against proof obligations.Source: §III · p. 5

IV. METHODOLOGY

  • The framework emits restricted SMT-LIB2 helpers that enter PDR through predicate generalization, clause injection, or property-strengthening refinement.The verifier parses and binds helpers before consuming them; the workflow returns a safe proof with an invariant or an unsafe counterexample.Source: §IV · p. 5, Figure 3 · p. 5

A. Restricted SMT-LIB2 Helper Interface

LLM4PDR routes typed SMT-LIB2 hints into word-level PDR while keeping their use subject to verifier-side checks. COI-filtered prompts provide design context, and helper predicates let inductive generalization preserve useful word-level structure.

A. Restricted SMT-LIB2 Helper Interface

  • The restricted SMT-LIB2 interface dispatches predicate, clause, and assertion declarations to distinct verifier paths, where each type is validated before use.Predicates supply candidate atoms for MIC, clauses are candidate frame lemmas, and assertions tentatively strengthen the target property.Source: A. Restricted SMT-LIB2 Helper Interface · p. 6

B. Prompt Construction and Helper Synthesis

  • A fixed prompt combines the available RTL or BTOR2 context with a few-shot example, mode-specific instructions, and strict SMT-LIB2 output constraints.Generated artifacts are parsed, type-checked, and validated before the model checker uses them.Source: B. Prompt Construction and Helper… · p. 6, Figure 5 · p. 6
  • COI analysis filters the prompt to property-relevant state variables and transition fragments without changing the transition system, target property, or PDR proof obligations.On representative HWMCC instances, this pruning removes 52.35%–82.49% of state variables from the prompt.Source: B. Prompt Construction and Helper… · p. 6

C. LLM-Guided Predicate Generation

  • Bit-level CTI cubes expose individual bit assignments rather than the high-level arithmetic relations that may be needed for an inductive invariant.In the xp2 example, the useful relation is y = x + 2.Source: C. LLM-Guided Predicate Generation · p. 7
  • Two-phase MIC first freezes matched helper predicates while pruning bit-level literals, then removes redundant helpers through inductive checks to retain a compact blocking lemma.This prevents ordinary MIC from dropping every matched helper predicate while minimizing the cube.Source: C. LLM-Guided Predicate Generation · p. 8, Figure 7 · p. 8
  • LLM-generated predicates do not enter a frame directly; the verifier checks that the resulting clause satisfies PDR’s requirements.The LLM proposes candidate relations, while the verifier retains control of proof soundness.Source: C. LLM-Guided Predicate Generation · p. 8

D. LLM-Guided Clause Generation

Clause generation proposes complete frame lemmas before the main blocking loop, giving PDR a potentially stronger initial frame. Verifier checks govern insertion into F1, and later propagation determines whether a clause remains useful.

D. LLM-Guided Clause Generation

  • Clause generation proposes complete lemmas up front, rather than waiting for CTIs to guide discovery of the arithmetic relation through local bit-slice lemmas.For xp2, the desired relation is y = x + 2; clauses may also be disjunctions combining word-level and bit-level conditions.Source: D. LLM-Guided Clause Generation · pp. 8–9
  • Irrelevant side-loaded clauses can slow SAT queries and steer search toward unproductive regions, so each proposed formula is treated as a candidate rather than a trusted invariant.Verifier-side sanity checks screen clauses before insertion into F1.Source: D. LLM-Guided Clause Generation · p. 9
  • A side-loaded clause enters F1 only after checks establish that initial states satisfy it and one-step successors satisfy its primed form.Ordinary PDR propagation then determines whether the clause advances to later frames.Source: D. LLM-Guided Clause Generation · p. 9
  • A candidate that passes the initial F1 checks can still fail to propagate, so only clauses that satisfy later ordinary checks persist in the proof.In the xp2 example, y = x + 2 is side-loaded into F1 and propagates.Source: D. LLM-Guided Clause Generation · p. 9

E. LLM-Guided Assertion Generation

Helper assertions tentatively strengthen the target property with LLM-proposed relations. Counterexample-guided refinement removes falsified helpers while distinguishing a genuine violation of the original property from an overstrong helper set.

E. LLM-Guided Assertion Generation

  • The verifier forms a strengthened property by conjoining the target property with active helper assertions, then asks PDR to prove it.Because the strengthened property implies the original, a successful proof establishes the original property as well.Source: E. LLM-Guided Assertion Generation · p. 9
  • The same relation can serve as a predicate, clause, or assertion, but an assertion is consumed by augmenting the target property rather than by MIC or frame insertion.For xp2, the augmented property exposes y − x = 2 alongside x < y.Source: E. LLM-Guided Assertion Generation · pp. 9–10
  • If an unblockable bad cube violates the original property, it is a real counterexample; otherwise, the verifier removes the helper assertions falsified by that cube and restarts.The refinement retains helpers that evaluate true on the cube.Source: E. LLM-Guided Assertion Generation · pp. 9–10
  • When every helper assertion is filtered out, the procedure reduces to ordinary PDR on the original property.The assertions are tentative augmentations, not assumptions added to the transition relation.Source: E. LLM-Guided Assertion Generation · p. 10

A. Setup and Baselines

The evaluation spans benchmark suites covering arithmetic datapaths, mixed control and datapath, HLS pipelines, and annotated open-source RTL. LLM4PDR runs use one fixed prompt template and a cap of five generated artifacts per instance and guidance mode.

A. Setup and Baselines

  • Four suites cover arithmetic micro-benchmarks, HWMCC designs, HLS-generated Kalman-filter kernels, and annotated bus interconnects and DDR3 controllers.The HLS properties encode bit-exact equivalence between independently pipelined implementations.Source: A. Setup and Baselines · p. 10
  • All runs use GPT o3, a fixed prompt template without benchmark-specific tuning, and up to five helper artifacts per instance and guidance mode.The artifact type varies by mode: predicate, clause, or assertion declarations.Source: A. Setup and Baselines · p. 10

B. Arithmetic Benchmarks

LLM-generated helper artifacts improve results on the 33 arithmetic micro-benchmarks, with assertion guidance solving the most cases. The suite tests whether helpers expose word-level relationships needed for compact inductive invariants.

B. Arithmetic Benchmarks

  • The 33 intentionally small benchmarks test whether helpers expose datapath equalities, bounds, and guarded relations needed for compact inductive invariants.Comparisons include Pono IC3bits, AVR, DreamMiner, and an IC3ng ablation without LLM-generated artifacts.Source: B. Arithmetic Benchmarks · p. 10
  • 28 of 33 cases are solved by LLM2Assert, versus 13 by Pono and 11 by AVR.LLM2Predicate and LLM2Clause each solve 23 cases; DreamMiner solves 19.Source: B. Arithmetic Benchmarks · p. 10
  • All three LLM4PDR variants outperform the deductive baselines, and LLM2Assert has the lowest cactus-plot curve over most of the solved range.The passage attributes the largest gain to assertion-guided search when generated helper facts align closely with the target property.Source: B. Arithmetic Benchmarks · p. 10

C. HWMCC Benchmarks

Across heterogeneous HWMCC instances, LLM guidance is not uniformly best, but different helper modes lead on different designs. On the DSP instance intersymbol_conv, LLM2Predicate cuts runtime sharply relative to the baselines.

C. HWMCC Benchmarks

  • The evaluation covers twelve HWMCC instances spanning accelerators, embedded CPUs, a DSP kernel, peripheral and storage controllers, and a video interface.Table II reports wall-clock runtime.Source: C. HWMCC Benchmarks · p. 10, Table II · p. 11
  • 3.06 s: LLM2Predicate proves intersymbol_conv, while Pono, AVR, and DreamMiner time out and unguided IC3ng takes 613.64 s.The passage identifies this as an example of helper predicates supplying a compact word-level explanation the unguided engine does not quickly discover.Source: C. HWMCC Benchmarks · pp. 10–11
  • LLM2Assert is fastest on two of three marlann_cp_* accelerator instances, while LLM2Clause is fastest on the third.Both variants improve over Pono, DreamMiner, and the IC3ng ablation on that family.Source: C. HWMCC Benchmarks · p. 10
  • HWMCC results are heterogeneous: guidance is not uniformly best on small instances, but different modes lead on harder cases, including intersymbol_conv, qspiflash, and zipcpu.The benchmark mix spans accelerators, CPU cores, DSP kernels, storage controllers, and video interfaces.Source: Table II · p. 11, C. HWMCC Benchmarks · p. 11

D. HLS–SEC Safety Kernels

Across arithmetic, HWMCC, HLS–SEC, and open-source RTL benchmarks, LLM4PDR modes improve different parts of proof search. The reported gains vary by design class, and an ablation indicates that helpers contribute beyond engine changes alone.

E. Open-Source RTL Designs with Assertions

  • LLM2Predicate has the best runtime on five of six open-source RTL cases and gives roughly 3–5× speedups over Pono on DDR3 controllers.The suite includes pipelined AXI bridges and DDR3 controllers with long control pipelines and wide datapaths.Source: Table IV · p. 12, E. Open-Source RTL Designs with… · p. 12

D. HLS–SEC Safety Kernels

  • LLM4PDR variants complete Kalman3 and Kalman4, where Pono, AVR, and the ablation time out; LLM2Clause is fastest among the variants on both, finishing in about one hour.The HLS–SEC suite uses fixed-point Kalman-filter kernels with independently pipelined implementations and long pipeline dependencies.Source: D. HLS–SEC Safety Kernels · pp. 11–12

F. Ablation: IC3bits vs. IC3ng

  • Without helpers, IC3ng shows both improvements and regressions against IC3bits; enabling helpers on the same IC3ng engine yields substantial additional speedups on several benchmarks.For intersymbol_conv, LLM2Predicate reduces runtime from 613.64 s to 3.06 s.Source: Figure 10 · p. 12, F. Ablation: IC3bits vs. IC3ng · p. 12

VI. CONCLUSION

  • Across arithmetic, HWMCC, HLS–SEC, and open-source RTL benchmarks, assertion guidance is strongest on arithmetic, clause guidance on deep HLS pipelines, and predicate guidance on open-source control-plus-datapath designs.The ablation against unguided IC3ng indicates the gains come from generated helper artifacts rather than an engine swap alone.Source: §VI · p. 13
Loading 2609.30131v1…