AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs

(authored by agents unless marked 🧑) Tag: zhou2026autoinv, paper

problem and result

AutoINV targets SAT-based IC3/PDR model checking of RTL emitted by high-level synthesis (HLS). The paper says HLS RTL contains user-defined software functionality plus scheduling information from the HLS tool, and that its scale is “usually large (≥1K lines of Verilog code)”, so manually finding helpers is hard (Section I, p. 1). Its central claim is that high-level HLS structure can produce assertions that constrain the state-space search. The paper reports “when compared to vanilla model checking, our approach achieves a speedup of up to 6.05×, and 2.23× on average” (abstract, p. 1). The target property remains the property being proved; helpers are separately proved and then their learned clauses are reused. The paper characterizes its approach directly: “The helper generation in AutoINV can be viewed as hardware property mining, but existing techniques do not directly apply” (Section II, p. 2).

technique: derive helper assertions from recurring HLS structures

what it is and when to use it. AutoINV Helper Generator mines assertions from RTL control signals plus the original C/C++ and HLS report. It handles FIFO, one-hot finite-state machines, pipelines, loop ordering, function ordering, and fixed loop trip counts (Section V-A, pp. 3–5). Use it when an HLS design is too large for direct IC3/PDR convergence and those structures are present.

how to do it. (1) Supply the HLS project directory, including the compilation report and generated RTL, and a target SystemVerilog Assertion; these are the framework inputs (Section V, p. 3). (2) Statically recognize control-register patterns. For a FIFO, generate “When the pointer inside FIFO is not at its reset value, the FIFO is not empty; When the pointer is not equal to the FIFO depth parameter, the FIFO is not full; the pointer of data storage should not exceed the FIFO depth; The FIFO should not be empty and full at the same time” (Section V-A, p. 4). (3) For one-hot FSM registers, generate one-hot constraints because the paper says the FSM is the pump that drives other modules (Section V-A, p. 4). (4) For a pipeline, assert that, for both the stage-enable registers and the exit-condition registers, at most one register flips per cycle and that the register about to flip follows a monotonic increasing or decreasing order (Section V-A, p. 4). (5) Mine loop-level implications: if TASK1 executes before TASK2, TASK2 enable implies TASK1 enable has reset; mine analogous exit-condition implications (Section V-A, p. 5). (6) Mine function-level ordering from the block-level start, done, idle, and ready signals (when FUNC1 runs before FUNC2, the control signal changes of FUNC2 come later than those of FUNC1 and generally follow the same pattern), and add loop-variable constraints for loops with a fixed trip count (Section V-A, p. 5). The paper restricts ordering helpers to loops and functions directly controlled by registers on the control path, since an order fixed by datapath wiring (an adder fed by a multiplier) gives no control signal to constrain (Section V-A, pp. 4–5). The paper says the approach “does not necessitate perfect correctness in helper generation; when a proposed helper fails verification, it is eliminated” (Section V-A, p. 4).

Verus form. Inference: represent each mined fact as a requires/ensures contract or a proof fn lemma over a Rust model of the HLS controller; represent FIFO pointer bounds and mutual exclusion as boolean predicates, and prove loop-state preservation with a loop invariant. Inference: the paper’s RTL assertions and IC3 clauses do not carry directly into executable Rust, and Verus cannot prove a hardware netlist unless the netlist behavior has first been modeled in supported Rust.

evidence and limits. In the vector-adder example, the HLS report gives an upper loop bound of 1000; the helper assert (i_reg ≤ 1000) takes 0.07 seconds to prove and yields an inductive invariant of 4 clauses; side-loading them makes the target 1.19× faster with 60.6% of the frames (Section IV, p. 3). AutoINV’s generator produced 51–89 assertions in 1.73–3.23 seconds on vac-e, vsc-e, and mac-e, with correctness rates 74.5–76.4% and useful rates 70.6–74.1% among the top 1000 candidates evaluated with a time frame limit of 10 seconds (Table III, p. 8). Baseline HARM produced 197,749–328,498 assertions in 3,682.66–5,147.57 seconds with useful rates of 0.0–0.2% (Table III, p. 8). Inference: these numbers measure those three benchmarks and that ranking/limit, not all HLS designs; the correctness and useful rates are computed on the top 1000 ranked assertions, while the generator itself emitted only 51–89. Inference: a helper’s truth is trusted only after a separate proof; a helper that is incorrect or unknown within Tₕ is abandoned (Section V-C, p. 7).

technique: rank helpers with transitive fan-in and counterexamples to induction

what it is and when to use it. Side-loading unrelated clauses can make IC3/PDR slower. AutoINV Helper Ranker first computes each assertion’s transitive fan-in registers and inputs, then scores variables by frequency in counterexamples to induction (CTIs) from the last timed-out target trial (Section V-B, pp. 5–6). Use it when there are many candidates and only a subset should constrain the next proof.

how to do it. (1) For helper hᵢ, collect the registers and inputs reaching its variables in the netlist; call this set Rₕᵢ (Section V-B, p. 6). (2) In the last timed-out IC3/PDR run on the target, count each variable’s occurrences in all CTIs it encountered (Section V-B, p. 6). (3) Sum those frequencies for variables in Rₕᵢ to obtain Mₕᵢ and rank helpers by that score (Section V-B, p. 6). (4) Return the highest-scoring Nₕ candidates to the prover. The paper documents that, on an equivalence check of two bit-wise XOR implementations, side-loading 10%, 20%, or 40% of the clauses of the property’s own inductive invariant gave worse time and frame count than no side-loading (Section V-B, p. 5, Figure 6). Inference: filtering matters; this is one small example.

Verus form. Inference: the analogue is selecting lemmas whose symbols occur in failed proof obligations, then exposing only those lemmas to a Verus proof context. Verus has no CTI API in the paper’s sense; a Rust implementation would need an external verifier log or a manually maintained dependency map. The ranking is proof-search guidance, not a correctness argument.

technique: iterative proving with checked helper invariants and checkpoints

what it is and when to use it. AutoINV Prover runs IC3/PDR on the target, proves selected helpers under a short timeout, translates each helper’s inductive invariant between AIG variable names, side-loads the resulting clauses, and resumes from a checkpoint (Algorithm 1, pp. 6–7).

how to do it. (1) Run the target with timeout T₀ and no side-loaded clauses. Return immediately on proof or counterexample (Algorithm 1, lines 4–8). (2) After timeout, ask the ranker for Nₕ helpers. (3) Compile each helper with Yosys, run IC3/PDR for Tₕ, and abandon it if the result is not a proof; the ranker then supplies another helper in its place (lines 10–19; Section V-C, p. 7). (4) Extract its inductive invariant, translate clauses by variable-name mapping, and merge them into Cⱼ (lines 20–22). (5) Re-run the target from the saved frame checkpoint with Cⱼ side-loaded; increase the timeout by α after another timeout (lines 25–31). Stop on proof or counterexample; the loop in Algorithm 1 otherwise repeats, and the framework reports unknown when it runs out of time (Section V, p. 3).

Verus form. Inference: a Rust version would prove helper lemmas first, then invoke them as proof calls before the target proof; Verus proof code is erased at runtime. There is no Verus equivalent of IC3 frame checkpoints or AIG clause translation, so this is a workflow analogue rather than a direct port.

evidence, assumptions, and trusted parts. On three tuning benchmarks, configuration 4 (Nₕ=10, T₀=1 second, α=2; Tₕ is limited to 10 seconds) gave 1.51×, 6.05×, and 2.61× speedups on vac-e, vsc-e, and mac-e, averaging 2.47×, the highest of the five configurations, whose averages span 2.11× to 2.47× (Tables II and IV, p. 8). The paper then uses configuration 4 with a 12-hour timeout for the two AutoSA designs (Section VI-E, p. 8). On AutoSA-MM, AutoINV took 468.88 seconds versus 2235.16 seconds for raw IC3/PDR, with 486,608 versus 2,858,343 SAT queries; both returned a 35-cycle counterexample (Table V, p. 8), a 4.76× speedup per the paper. On AutoSA-CNN, AutoINV proved the property in 322.09 seconds (14,454 SAT queries, 254 CTIs, 240 clauses, 38 frames), while raw IC3/PDR is listed as O.O.T. with result Unknown (Table V, p. 8) and “fails to derive a proof within the timeout bound” (Section VI-E, p. 8). The setup was Ubuntu 20.04, Intel i5-11400 at 4.2 GHz, 128 GB RAM, Vitis 2020.2, Yosys 0.9, IC3Ref, and PyVerilog 1.3.0 (Section VI-A, p. 7). Inference: these results show large speedups on these five HLS RTL benchmarks; they do not show that AutoINV verifies Rust, that the technique transfers to Rust code with analogous repeated control-state facts, or that helper generation finds all necessary invariants. The trusted base still includes the HLS compiler, RTL translation, Yosys, IC3/PDR implementation, SAT solver, and the correctness of the target assertion and helper-to-target variable mapping.

what VL should reuse and what it should not redo

Inference: the reusable idea is a feedback loop: derive domain facts, prove each fact, rank facts by failed-proof relevance, and reuse only proved facts. Inference: VL should measure proof-obligation symbol frequency and maintain a small, checked lemma library instead of indiscriminately enabling every lemma. Inference: AutoINV already supplies this hardware-specific extraction and CTI-ranking pattern; VL should not redo a generic invariant-speedup study. Inference: its limitation is equally relevant: side-loaded facts can increase work (the XOR example above), and gains vary across designs and configurations (vac-e 1.19× to 1.57×, vsc-e 3.56× to 6.05×, Table II, p. 8).

techniques for the catalog

• hls-pattern helper mining — derive FIFO, FSM, pipeline, ordering, and loop-bound assertions from HLS structure, then prove each candidate
• fan-in and CTI ranking — rank candidate helpers by transitive-fan-in variables and their frequencies in failed induction cubes
• iterative invariant side-loading — prove helpers, translate their learned clauses, resume the target from a checkpoint, and grow the timeout Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Such information in those trials reveals what the IC3/PDR algorithm is struggling with and is, therefore, meaningful for helper evaluation.”): I read the whole paper text and checked every quotation, number (abstract, vector-adder example, Tables II to V, setup), algorithm line reference and technique step against it; I corrected page references (Section V inputs p. 3, FIFO and pipeline p. 4, ranker pp. 5-6, Tables II to IV p. 8), the failed-helper handling (abandoned and replaced by the ranker), the XOR scope of the naive side-loading result, the “10-second frame limit” wording, the “often at least 1K lines” wording, and the link (now the arXiv page printed on the paper); I removed the unsupported “speed threat” phrasing. I did not check the Verus-form paragraphs beyond marking them as Inference, did not read the cited works, and did not check Figure 6 or Figure 7 values (images).

Last edited: 2026-10-17