equiv_receipt.tseitin

Gate-netlist to CNF, and equivalence miters — standard library only.

A miter of two circuits is satisfiable exactly when they differ on some input. So unsatisfiability of the miter is equivalence, and a DRAT refutation of the miter is a checkable proof of it.

Clause = typing.List[int]

class Netlist:

A tiny combinational netlist over AND / OR / NOT / XOR gates.

Inputs are named; every gate produces a new named signal. Deliberately minimal — this exists so the package is usable and testable without a synthesis tool, not to replace one.

Netlist(inputs: Sequence[str])

inputs

def var(self, name: str) -> int:

def NOT(self, out: str, a: str) -> str:

def AND(self, out: str, a: str, b: str) -> str:

def OR(self, out: str, a: str, b: str) -> str:

def XOR(self, out: str, a: str, b: str) -> str:

def BUF(self, out: str, a: str) -> str:

An alias. Needed when a signal must be renamed rather than computed.

def CONST(self, out: str, value: bool) -> str:

A signal pinned to a constant, as a unit clause.

Sequential unrolling needs it for latch reset values; combinational use does not.

clauses: List[List[int]]

def n_vars(self) -> int:

def miter( build_a, build_b, inputs: Sequence[str]) -> Tuple[List[List[int]], Netlist]:

Build a miter CNF for two single-output circuit builders.

build_a(net, prefix) -> output_signal_name. The returned CNF is satisfiable iff the two circuits differ on some input assignment; therefore UNSAT means equivalent.