Add dynamic SRM and incremental simulation into &scorr -i ; Fix a bug of &scorr -i ;

[zxxr1113]

Summary

This PR adds three optimizations to the &scorr -i incremental refinement loop: -D (dynamic SRM construction), -I (persistent event-driven resimulation), and -s (skip fail-only resimulation). It also fixes a correctness bug in -i's TFO traversal caused by missing speculative alias dependencies.

-D: Dynamic SRM Construction

-D replaces per-round SRM rebuild with a persistent, CO-less pCore. The core is append-only — new AND gates are added only on cache misses, and existing gates are never rewired. A literal cache maps (frame, host object) to pCore literals and is invalidated per round by the TFO mask. Proof roots are solved directly on the resident Cbs manager without per-round view allocation or CO construction. Compaction cold-rebuilds the core when it grows beyond 4× the post-rebuild baseline.

-I: Persistent Event-Driven Resimulation

-I maintains persistent simulation state across rounds and propagates only changes from new CEX lanes through an event queue, rather than sweeping the full unrolled AIG each round. A class-cone filter limits propagation scope. When the local event path is too wide, shape-incompatible, or coverage is incomplete, the implementation falls back to full resimulation, preserving correctness.

-s: Skip Fail-Only Resimulation

When the current round's CEX store contains only trivial SAT or fail/timeout entries with no real CEX patterns, resimulation is skipped. Trivial SAT entries are still handled by direct splitting, and fail entries are handled conservatively by Gia_ManCheckRefinements.

-i Bug Fix: Alias Dependency

The old incremental TFO traversal followed only physical AIG fanout edges, missing implicit representative → member alias edges from speculative reduction. When a representative's literal changed due to class refinement, members referencing it and their fanout cones were incorrectly treated as unaffected. The fix adds adjacency from each representative to all class members, so TFO BFS covers the full speculative SRM dependency graph.

Algorithm

-D: Persistent pCore with Speculative Literal Cache

init:
    create pCore with stable CIs (RIs, ROs, framed PIs)
    initialize empty vSpecLits cache

per round:
    invalidate vSpecLits for objects in active TFO mask
    for each active proof root:
        SpecLit(obj, frame):
            if cache hit → return cached literal
            if obj has representative:
                build SpecLit(repr, frame), apply phase difference
            else:
                recursively build real fanin logic via pCore
            cache and return result
        push root literal to vOutLits
    Cbs_ManSolveRoots(pCbs, vOutLits)

compaction (if pCore size > 4 × baseline):
    rebuild pCore from scratch, reconstruct live cones on demand

-I: Persistent Event-Driven Resimulation

init:
    allocate persistent (frame, object) value storage

per round:
    classify CEX entries (real / trivial / fail)
    if no real CEX → skip (handled by -s path)

    load new CEX lanes into persistent input bank
    detect changed input words

    if local event path not allowed (too wide / shape mismatch):
        fallback full resimulation

    build or reuse class-cone filter from current proof outputs
    propagate changes through frame-aware event queue:
        for each changed input word:
            push fanout nodes to event queue
        while queue not empty:
            evaluate node, if value changed → push fanouts

    if coverage incomplete → fallback full resimulation
    commit transaction → refine affected classes

-s: CEX-Guided Resimulation Gate

per round after SAT/Cbs solving:
    nRealCex = count of entries with nLits > 0
    if nRealCex == 0 and -s enabled:
        skip resimulation
        handle trivial SAT by direct split
        handle fail entries via Gia_ManCheckRefinements
    else:
        run resimulation (full or -I)

Performance

High-Impact Cases (scorr runtime > 1.0s)

Benchmark	&scorr (s)	&scorr -i (s)	Speedup	Gate Red%	Latch Red%
transmitter.10.cil.aig	359.34	4.30	83.57x	-0.03%	0.00%
token_ring.12.cil-1.aig	145.26	4.85	29.95x	-0.04%	0.00%
Problem05_label49+token_ring.06.cil-2.aig	654.90	24.50	26.73x	-0.25%	0.00%
Problem05_label45+token_ring.13.cil-1.aig	1069.41	45.79	23.35x	-0.30%	0.00%
pc_sfifo_3.cil+token_ring.01.cil-2.aig	12.79	0.75	17.05x	-0.02%	0.00%
pc_sfifo_2.cil-2+token_ring.09.cil-1.aig	111.53	7.65	14.58x	-0.04%	0.00%
pc_sfifo_3.cil+token_ring.10.cil-1.aig	91.85	6.58	13.96x	-0.04%	0.00%
Problem05_label42+token_ring.04.cil-2.aig	252.98	20.36	12.43x	-0.56%	0.00%
elevator_spec2_product25.cil.aig	168.15	13.63	12.34x	-0.02%	0.00%
pc_sfifo_3.cil+token_ring.09.cil-2.aig	58.65	5.49	10.68x	-0.04%	0.00%

Performance Verification

~95% of optimized cases pass the existing dsec equivalence check. The remaining ~5% of cases cannot complete dsec runs due to dsec limits. A dedicated self-check algorithm for the incremental path is under active development.

Acknowledge

The core strategy for this new implementation was guided by Alan Mishchenko.