[alanminko]

Summary

pdr2 now accepts the initial value of each flop as 0, 1 or don't-care, and solves the problem in the original flop polarities. Before this change it assumed every flop starts at 0, as pdr does, which had three effects:

• Flops initialized to 1: the conversion to an AIG (Abc_NtkToDar) complemented them, so the invariant came out with inverted literals on those flops.
• Don't-care flops: the conversion set them to 0, with only a warning, and changed the user's network in place. So pdr2 could report "proved" when the property fails from some initial state.
• Running undc first (logic; undc; st; zero) fixes the semantics, but the counterexample and the invariant then describe the transformed design. Mapping the counterexample back exists (undc -c). Mapping the invariant back does not, and it is not a substitution: the correct invariant is "the initial states, or the transformed invariant with the control flop set". That is not a clause set unless each clause is multiplied out per initialized flop.

pdr is unchanged.

Changes

Interface

• New entry point Pdr2_ManSolveInit( pAig, vInit, pPars ). vInit gives 0, 1 or 2 (don't-care) per flop; NULL means all 0. Pdr2_ManSolve() calls it with NULL.
• Abc_NtkDarPdr2() reads the initial values from the latches and converts the network without complementing anything. Afterwards the network is left exactly as it was.
• For a combinational network, the pdr2 command now adds its dummy flop as next state 0 with initial value 0. The engine sees the same AIG as before, with all-zero initial values.

Engine

• Frame 0: gets unit clauses only for the flops with a defined value. The frame-0 cubes follow the same rule.

• Which cubes intersect the initial states: a cube meets them unless it has a literal opposite to a flop's defined value. A literal of a don't-care flop never counts. This test is used by:

  • MIC (down, CTG);
  • the inductive core of the SAT-core lifting;
  • the abstraction's projection fixup;
  • the invariant checker.

• Counterexample: its register bits hold the initial state of the trace, built from:

  • the first cube of the obligation chain;
  • the defined values of the flops not in the cube;
  • 0 for the remaining don't-care flops.

  No extra SAT call is needed, because lifting guarantees that any state in the cube works. The ternary and concrete simulations of the abstraction checks start from the same state.

• Final check of the counterexample: it must start in an initial state, and Saig_ManVerifyCex must reproduce the failure.

Designs derived inside pdr2

• Abstraction runs with a reset flop: a flop with a defined value is gated to that value in the reset cycle, with AND for 0 and OR for 1. Don't-care flops are left ungated and keep the don't-care value. A counterexample from these runs takes the run's values for the don't-care flops.

• BMC stage: BMC assumes all-zero initial values, so it runs on a zero-init copy, and its counterexample is mapped back. In the copy:

  • flops initialized to 1 are complemented;
  • each don't-care flop is replaced in the first frame by a new input, selected by an extra register.

  For all-zero designs nothing is copied.

• -q (scorr): skipped unless all initial values are 0.

-d output

• The design file is written with its initial values, using AIGER 1.9 latch lines next init, where init is 0, 1, or the latch literal for don't-care.
• The invariant is over the original flops.

What happens to the counterexample and the invariant

Both describe the original circuit directly, so neither needs mapping back.

The counterexample

• It keeps the original inputs, with no extra inputs from undc, and the same number of frames.
• Its register bits hold the real initial state: 1 for flops initialized to 1, and the values chosen for don't-care flops.
• ABC's checkers (Abc_NtkVerifyCex, Saig_ManVerifyCex, Gia_ManVerifyCex) take each flop's starting value from those bits, not from the latch's init setting. Before this change the bits were all 0, so on a design with flops initialized to 1 the counterexample checked out only on the internal complemented copy. Now testcex -a confirms it on the original network.

The invariant

• It is a set of clauses over the original flops in their original polarities: no inverted literals and no undc control flop. For the original design:
  • every initial state satisfies it;
  • it is preserved by one step of the transition;
  • it implies the property.
• It is the same set of lemmas the search found, with no multiplying out per initialized flop.
• With don't-care flops, a clause can exclude the initial states only through flops with defined values. That can make invariants larger or harder to find, but it is a property of the problem, not of the encoding.
• -d writes the design with its initial values next to the invariant.
• As before, when an abstraction run with the reset flop finishes the proof, the invariant is over that run's gated design (one extra flop). That design is the one written by -d, also with its initial values.

Designs whose flops all start at 0 get exactly the same search, counterexamples and invariants as before.

Testing

• No change on all-zero designs: the 77 IWLS'17 examples at 60 s, 4 jobs (none has a non-zero initial value). Results and solver propagation counts are identical to the previous build on all 66 examples it solves within 60 s.

• Random circuits with random initial values: 3–6 flops; each flop is 0, 1 or don't-care. A local harness ran 17 pdr2 configurations on 600 circuits each, about 77% of them with non-zero initial values. Every configuration passed:

  • results agree with exhaustive reachability from all initial states;
  • every counterexample starts in an initial state and reproduces the failure;
  • every dumped invariant was checked by brute force: it contains the initial states, is inductive and excludes the bad states;
  • the dumped design carries the initial values;
  • invariants over the gated design of the abstraction runs were checked too.

• End to end: 48 variants of IWLS examples with 10% of the flops at 1, at don't-care, or both. Three routes agree on 47 of them; on the remaining one, pdr ran out of time at 30 s while both pdr2 routes proved it:

  • pdr2 on the original files;
  • the previous pdr2 after logic; undc; st; zero;
  • pdr after the same commands.

  All 29 counterexamples pass testcex -a on the original networks. All 19 proofs pass the built-in invariant verification, and their dumped designs carry the input's initial values.

• Side finding: undc on a strashed network does nothing. Without logic first, the old route silently treats don't-care values as 0, and it proved 12 of these variants that actually fail.

🤖 Generated with Claude Code