equiv_receipt.seq

Sequential equivalence by k-induction, with a re-derivable receipt.

Combinational equivalence is one SAT call. Sequential equivalence is not: two circuits with state agree only over reachable states, and reachability is the hard part. This module proves it by k-induction, which is a standard technique — Sheeran, Singh and Stålmarck introduced it; Bradley, Biere, Heljanko and others developed the certification of it. Nothing about the method is new here. What this module adds is that the result arrives as an artifact a third party can re-derive.

Two arguments are available, and the receipt records which one carried the result.

Register correspondence — the practical one. The invariant is "corresponding latches hold equal values", discharged as three obligations: it holds at reset, one step preserves it, and it implies equal outputs. When that goes through, a single step of induction settles every time step.

k-induction on outputs — the general one, for designs whose state encodings do not correspond. From the reset state the outputs agree at times 0 … k-1; and from an arbitrary state, agreement at k consecutive times implies agreement at the next.

Reset-state base cases run first under either argument, because a failure there is a real counterexample rather than an artefact of an unreachable assumed state. Every obligation is discharged by a SAT solver and carries a DRAT proof, so the receipt contains proofs, not assurances.

A note on why the first argument exists: plain k-induction on the output property alone will essentially never prove two independently-encoded state machines equivalent, because an arbitrary assumed state can have the two circuits in different — but output-agreeing — states, from which they diverge. That is not a bug in k-induction; it is why practical sequential equivalence checking looks for a state invariant. Shipping only the general argument would have been a feature that abstains almost always.

The third outcome is the honest one. Both arguments are sound but incomplete: they can fail on circuits that are genuinely equivalent, because the assumed states need not be reachable. When the reset-state base cases pass and neither inductive argument closes, the verdict is UNDECIDED-AT-K — an abstention. It is not a failure of the circuits and it is not a pass. Raising k may resolve it; nothing here pretends otherwise.

The encoder gap is closed here. A combinational receipt commits the CNF bytes and a prose description of the circuits, so a verifier can detect a swapped formula but cannot confirm the formula is the circuits. A sequential design is committed as machine-readable data, so verify_seq_receipt() re-encodes every obligation from the design and compares it to the committed formula. A receipt whose CNF does not correspond to its circuits is rejected.

SEQ_FORMAT = 'equiv-receipt-seq/1'

ENCODER_ID = 'equiv-receipt.unroll/1'

BINARY_OPS = {'XOR', 'OR', 'AND'}

UNARY_OPS = {'BUF', 'NOT'}

EQUIVALENT = 'EQUIVALENT'

COUNTEREXAMPLE = 'COUNTEREXAMPLE'

UNDECIDED = 'UNDECIDED-AT-K'

class DesignError(builtins.ValueError):

A sequential design that cannot be interpreted.

def validate_design(d: Dict) -> Dict:

Check a design is well formed and in a canonical, re-encodable shape.

Rejects rather than repairs. A design that has to be guessed at cannot be re-encoded identically by someone else, which would defeat the point.

def design_digest(d: Dict) -> str:

def build_obligation(a: Dict, b: Dict, k: int, *, kind: str, at: int = 0) -> List[List[int]]:

CNF for one proof obligation. UNSAT is the desired answer in every case.

kind is "base" (differ at time at, from the initial state) or "step" (agree at 0..k-1 from an arbitrary state, differ at k).

Deterministic in its inputs, which is what lets a verifier re-encode and compare bytes.

def prove_sequential_equivalence( a: Dict, b: Dict, *, k: int = 1, refute=None, name_a: str = 'A', name_b: str = 'B', seed: int = 1) -> Dict:

Prove a and b sequentially equivalent, or find a counterexample.

refute(clauses) -> {"unsat", "drat", "model"}; defaults to the bundled solver. Pass equiv_receipt.solver.refute() for a real one.

Two arguments are attempted, in this order, and the receipt records which one carried the result:

Register correspondence — the stronger invariant "corresponding latches hold equal values". Three obligations: it holds at reset, it is preserved by one step, and it implies equal outputs. When it goes through, one step of induction settles every time, which is why it is tried first.
k-induction on outputs — the general argument, for designs whose state encodings do not correspond.

Base cases from the reset state are always run first, because a failure there is a real counterexample rather than an artefact of an unreachable assumed state.

def build_seq_receipt( *, verdict: str, design_a: Dict, design_b: Dict, k: int, obligations: List[Dict], counterexample: Optional[Dict] = None, name_a: str = 'A', name_b: str = 'B', seed: int = 1, method: str = 'k-induction') -> Dict:

def verify_seq_receipt(receipt: Dict) -> Dict:

Re-derive a sequential receipt from scratch. Never reads the verdict.

Four things are checked, and the third is the one a combinational receipt cannot do: the CNF of every obligation is re-encoded from the committed design and compared, so the formula is proven to be the circuits.

def write_seq_receipt(path, receipt: Dict):

def read_seq_receipt(path) -> Dict: