Sec

[nanocoh]

• Allowing same-named resetless state bits to seed frame-0 correspondence when explicit init does not conflict, then only promoting them into the induction invariant after reset/bootstrap proves they survive.

• Adding a SAT equivalence fallback for Boolean-equivalent but structurally different next-state cones.

SEC runtime, convergence, and regression-workflow improvements

This PR is a large runtime/convergence update for the SEC engines, focused on making k_induction, imc, and especially pdr usable on both large ASIC-style regressions such as BlackParrot and smaller designs such as AES, GCD, IHP GPIO, and TinyRocket.

The main theme is to stop building one huge proof obligation too early. The flow now slices SEC obligations by output support, lazily materializes transition cones, reuses reset/frontier proof facts, and escalates PDR precision only when cheaper stages produce an abstract counterexample.

Regression workflow changes

• Split the SEC regressions into separate engine workflows: regress-ki, regress-imc, regress-pdr, while keeping the LEC flow separate as regress-lec.

• Added regress/run_sec_strategies_regress.sh so the same SEC regression harness can run k_induction, imc, pdr, or all three locally.

• The SEC regression helper rewrites the original LEC config into SEC mode, strips CNF-export-only options, supports engine=<name>, max-k=<n>, compact, expect-equivalent, and expect-different, and writes per-engine logs under regress-output.

• The helper now streams tool output and emits a heartbeat for long solver runs, which makes CI logs easier to diagnose when PDR is doing real work rather than hanging.

• The split workflows build an optimized Release binary with LTO and run the external SEC cases plus TinyRocket equivalent/different checks per engine.

Shared SAT and encoding infrastructure

• Changed the embedded Kissat build from --ultimate to --compact --quiet --no-proofs because --ultimate compiles out runtime options. SEC now needs runtime Kissat profiles for different query types.

• Added solver status handling so callers can distinguish SAT, UNSAT, and UNKNOWN, instead of treating every non-SAT result the same.

• Added Kissat variable reservation to avoid repeated internal variable-vector growth while emitting large Tseitin encodings.

• Added Glucose assumption solving with optional conflict/propagation budgets and failed-assumption core extraction. This is used by reset-frontier reachability checks and PDR refinement.

• Added separate solver profiles for SEC cone proofs, PDR predecessor queries, and reset-expression proofs. Cone proofs keep an UNSAT-oriented profile, PDR predecessor queries use a SAT/focused profile, and reset-expression proofs use a bounded proof-oriented profile.

• Extended the SAT encoder with frame-local symbol aliases. Equality facts such as startup/bootstrap/inductive state correspondences can now be encoded by sharing literals inside the relevant frame instead of adding many equality clauses.

• Added arena-backed formula encoding caches in FrameFormulaEncoder to reduce allocation churn in short-lived PDR and BMC queries.

• Added support for encoding only selected leaf symbols, creating missing leaves only when requested, and applying symbol maps while encoding lazy transition expressions.

SEC problem construction and extraction

• Added lazy transition storage to KInductionProblem. Large designs no longer remap every next-state expression into the shared SEC symbol space before proof slicing. KI and PDR now remap only the transition equations pulled into the current COI.

• Added TransitionExprResolver, which provides eager or lazy transition lookup, transition support caching, node-count hints, state-symbol lookup caching, and complemented-state reverse lookup.

• Stored initial state assignments separately from the monolithic initial-condition formula. This lets COI-reduced BMC encode only relevant init facts.

• Reset-name handling now recognizes common input suffixes like reset_i and rst_ni, so reset/bootstrap inference is consistent across extraction, reachable-state analysis, and proof construction.

• PDR skips expensive global reset-bootstrap equality mining for very large state spaces and relies instead on local reset-frontier validation and PDR refinement.

• Opaque internal SEC boundary inputs are now carried forward as environment inputs, so compact SEC rebuilds do not reference symbols missing from the shared proof symbol space.

• Sequential extraction now rebuilds only next-state transition cones required by covered outputs and their state dependencies, instead of materializing all state transitions up front.

• Connectivity-skip propagation was rewritten to precompute reverse dependencies with reusable scratch storage and TBB parallel scans. This avoids repeatedly walking large BoolExpr cones when skipped state dependencies propagate.

Structural and reachable-state invariant work

• Structural state matching now uses arena-backed memoization and iterative DAG traversal instead of recursive per-root walks.

• State fingerprint refinement now reserves hash tables more deliberately and uses unordered maps for refinement signatures, reducing pre-proof runtime on large designs.

• Abstract expression equivalence now supports caller-owned memoization so reset/bootstrap equality mining can compare many related expressions without redoing shared sub-DAG work.

• Reachable-state invariant construction now merges structural state correspondences with safe same-name startup correspondences.

• Reset/bootstrap equality derivation now has bounded SAT recovery for small ambiguous equality candidates. Structural and constant-derived equalities are used first; SAT is only spent under candidate/support budgets.

• Reset/bootstrap value derivation now uses iterative constant evaluation with arena-backed memoization, avoiding deep recursion and per-node allocation churn.

• Resetless/initless SEC now still uses structurally matched state correspondences as relational frame-0 strengthening facts, instead of forcing the engines to rediscover those equalities through output cones.

Output batching

• Added OutputBatching.cpp/h.

• Multi-output SEC properties are now split into support-bounded output batches. Each batch is still a real SEC conjunction, so proving all batches is equivalent to proving the full property.

• Batching is limited by output count and union support. This avoids one giant OR-of-all-output-bads query while also avoiding the old one-output-at-a-time behavior that repeated setup hundreds of times.

• Batch configuration mutates one shared KInductionProblem copy instead of copying the full state/transition/equality metadata for every output slice.

k-induction changes

• The k-induction schedule now checks frame 0 first, then for each k >= 1 tries the induction step before extending the base case.

• If the induction step does not close, the base query checks only the newly exposed frontier frame instead of re-solving a cumulative OR over all previous bad frames.

• A final cumulative base-case query remains as a safety net before returning inconclusive.

• Multi-output k-induction now runs over support-bounded output batches and recursively splits only inconclusive batches. Successful wide batches stay wide.

• The induction step now builds a true COI around the induction property, induction bad formula, and required transition targets.

• Inductive state equalities can be encoded as aliases in hypothesis frames, while the concrete base case remains unaliased where it must search real reachable prefixes.

• Simple-path constraints are bounded so they do not dominate large SEC cones.

IMC changes

• IMC now reuses the optimized shared base-case solver for counterexample checks.

• Before constructing an explicit exact reachable frontier, IMC tries an output-batched k-induction proof at the same depth.

• This gives large designs a cheap proof path when the exact-frontier construction would exceed practical size, while still preserving IMC’s exact-frontier path for cases where it is useful.

• The fallback induction proof is output-batched, so IMC no longer creates one giant all-output formula when the exact frontier path is too large.

PDR engine changes

• PDR now has tunable precision knobs: predecessor projection limit, precise bad-cube limit, exact-frame-clause mode, predecessor-query budget, projected-counterexample refinement, bounded root generalization, validated bad-formula learning, and exact reset-frontier checks.

• PDR predecessor queries now carry bounded predecessor cubes. Learned clauses are still justified by real UNSAT predecessor queries, but the carried obligation is projected to avoid enumerating enormous SAT models.

• Exact-frame retries are available when projected frame clauses are too weak. This lets the strategy start cheap and only pay for stronger frame clauses when needed.

• PDR now tracks query/stage statistics under KEPLER_SEC_PDR_STATS, including batch, stage, transition closure, projection limits, bad-cube limits, relation sizes, and predecessor-query behavior.

• Added reset-frontier reachability contexts and caches so repeated startup/post-reset cube checks reuse indexing, solver construction, failed assumption cores, and known unreachable cubes.

• Added one-shot, cached-assumption, shared-prefix, exact-target, and batched reset-frontier query variants. Different PDR stages can choose the cheapest sound query shape for the obligation.

• Added relaxed reset-frontier prechecks before the expensive exact Glucose assumption path. If the relaxed COI is already UNSAT, the exact query can be skipped.

• Added reset-summary prechecks as a bounded fallback, with resource limits and blocker learning, so AES/GCD-style reset obligations do not fall immediately into expensive full reset-frontier solving.

• Added reset-specialized constant/expression reasoning. PDR can prove many startup cubes impossible by symbolically evaluating reset/reset-release expressions before opening a SAT reset-prefix query.

• Added reset-expression canonicalization and structural implication checks to catch equivalent/contradictory reset expressions without SAT where possible.

• Added caches for reset-expression conflicts, reset-core implication, transition-impossible reset cores, and reset-expression budget skips so neighboring cubes do not rebuild the same reset proof.

• Added exact reset-frontier core extraction using Glucose failed assumptions. Smaller unreachable cores are reused as safe-prefix blockers for later cubes.

• Added predecessor-core generalization. Wide blocked cubes can be reduced using actual UNSAT predecessor cores, but the number of checks is bounded to avoid spending more time minimizing than proving.

• Added bad-formula validation and repair. When final PDR reaches an abstract bad trace that concrete BMC rejects, PDR can learn state-only CNF clauses for the validated bad formula instead of blocking one neighboring cube at a time.

• Added whole-batch validated bad-formula learning for small/controlled batches, which was important for BlackParrot because it lets PDR repair a 16-output batch as a batch rather than falling into per-output reset repair.

• Added per-output and reset-cube repair paths for smaller designs, with strict caps, so small AES/GCD/TinyRocket cases still benefit from exact reset repair without forcing BlackParrot through the same expensive path.

• Added concrete validation before accepting final singleton PDR counterexamples/equivalence decisions. This prevents projected PDR abstractions from reporting a false result.

• PDR propagation and bad-state checks can use exact frame clauses independently from predecessor projection. This keeps learned reset/bad-formula blockers visible where they matter without making every predecessor cube huge.

PDR strategy changes

• The top-level SEC PDR strategy no longer calls the full k-induction engine at max_k=0. It now performs only the cheap frame-0 base mismatch check before PDR starts.

• PDR runs over support-bounded output batches, prunes each batch relation to the relevant transition cone, and then escalates through staged precision retries.

• The staged flow starts with a compact projected relation, then widens the transition closure, then grows predecessor projection, then tries exact-frame PDR, and finally runs a final exact stage with validated bad-formula learning.

• Projected PDR stages can skip exact reset-frontier checks because the strategy validates PDR differences at the concrete SEC boundary before accepting them.

• The final exact stage keeps concrete validation and validated bad-formula repair enabled, but avoids the expensive per-output reset-frontier behavior that made BlackParrot regress.

• Batch splitting is delayed until the final exact stage fails to repair the batch. This avoids prematurely turning BlackParrot into hundreds of one-output PDR runs.

• For BlackParrot, the important convergence fix was restoring a larger batch shape and avoiding per-output reset repair in the final path. The working behavior used larger multi-output batches; the regressed behavior split too aggressively and spent minutes in reset-frontier/Glucose loops. The new flow keeps 16-output-style batches, uses whole-batch validated bad-formula learning, and only splits when the final exact batch really cannot be repaired.

• For smaller designs, the same machinery still converges quickly because relaxed reset-frontier checks, reset-summary prechecks, cached failed cores, and exact singleton validation handle the local reset obligations without requiring the heavyweight BlackParrot path.

Tests and examples

• Expanded SequentialEquivalenceStrategyTests heavily to cover the new KI, IMC, PDR, reset-frontier, batching, lazy-transition, bad-formula repair, and diagnostic paths.

• Added tests for reset/bootstrap induction, strengthened induction invariants, reset-frontier reachability caching, failed-assumption core reuse, prior-core blockers, checked reset-frame PDR properties, and concrete validation of projected PDR results.

• Added/updated TinyRocket SEC regression artifacts, including the CSRFile counterexample case used to ensure final PDR validation does not falsely prove an actually different design.

• Updated TinyRocket generated manifests/headers to the current Naja-generated artifact version.

Validation

Local regress-pdr validation completed all target designs with expected results.

Design	Expected result	Representative local time
AES	equivalent	~71s
GCD	equivalent	~6s
BlackParrot	equivalent	~301s
IHP GPIO	equivalent	~6s
TinyRocket Naja IF	equivalent	~6s
TinyRocket Verilog	equivalent	~6s
TinyRocket CSRFile	different	~6s
TinyRocket self	equivalent	~6s
TinyRocket Naja IF edited	completes	~181s
TinyRocket Verilog edited	completes	~116s

BlackParrot was also compared against the previously passing branch behavior. The passing comparison binary completed BlackParrot in about 493s locally, while this updated flow completed it in about 301s. The smaller AES/GCD regressions also moved from very long or non-terminating PDR behavior to minute/second scale.

[codecov]

Codecov Report

❌ Patch coverage is 94.33594% with 145 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
src/sec/strategy/StructuralStateInvariant.cpp	84.87%	85 Missing ⚠️
src/sec/strategy/ReachableStateInvariant.cpp	92.58%	44 Missing ⚠️
src/sec/strategy/SequentialEquivalenceStrategy.cpp	96.72%	8 Missing ⚠️
src/sat/SATSolverWrapper.h	97.61%	4 Missing ⚠️
src/sec/kinduction/SatEncoding.cpp	98.77%	2 Missing ⚠️
src/sec/model/SequentialDesignModel.cpp	98.96%	2 Missing ⚠️

📢 Thoughts on this report? Let us know!