A gate-level netlist miter can hold far more gates than any solver could take on output by output, yet equivalence checkers routinely decide such miters. The reason is that most of the netlist is shared structure: the two cones overlap almost everywhere, and proving the shared part once proves it for both sides. This lesson explains the mechanism so that a slow run can be diagnosed instead of feared.
This lesson has one job: show why a big miter is tractable, and what to check when it is not.
Structural hashing walks both cones from the inputs and gives an identical identifier to every gate with the same function and the same children. Gates with equal identifiers are merged: one copy serves both cones, so shared logic is solved once. What remains unmerged are the genuinely different regions.
SAT sweeping then works from the inputs toward the outputs. It simulates a few thousand random vectors and records a signature per node: the values that node took. Nodes with equal signatures are candidates for equivalence. Each candidate pair is asked to the solver: is there any input that distinguishes them? If no, the pair merges and everything downstream simplifies. If yes, the distinguishing input joins the simulation set, which refines every signature. The loop ends when every output pair has merged or a real mismatch reaches the comparator.
The script below models the loop on small Boolean networks. Six nodes get signatures over eight vectors; candidates with equal signatures are confirmed by exhaustive check, which stands in for the solver. Merges are counted. Then an injected pair shares signatures on the first vectors yet differs on one corner: confirmation catches it and refines the set. Both directions are asserted: real pairs merge, the impostor is caught.
import itertools
def truth_table(fn, n):
return tuple(fn(bits) for bits in itertools.product([0, 1], repeat=n))
def signatures(nodes, vectors):
return {name: tuple(fn(v) for v in vectors) for name, fn in nodes.items()}
def confirm(f, g, n):
for bits in itertools.product([0, 1], repeat=n):
if f(bits) != g(bits):
return False, bits
return True, None
N = 3
VEC = [(0,0,0),(0,0,1),(0,1,0),(0,1,1),(1,0,0),(1,0,1),(1,1,0)]
nodes = {
"and_ab": lambda v: v[0] & v[1],
"and_ab_dup": lambda v: v[0] & v[1],
"or_bc": lambda v: v[1] | v[2],
"xor_term": lambda v: v[0] ^ v[1] ^ v[2],
"impostor": lambda v: (v[0] & v[1]) & (1 - v[2]),
}
sig = signatures(nodes, VEC)
cands = [("and_ab", "and_ab_dup"), ("and_ab", "impostor")]
merges, caught = 0, []
for x, y in cands:
if sig[x] != sig[y]:
continue
ok, witness = confirm(nodes[x], nodes[y], N)
if ok:
merges += 1
else:
caught.append((x, y, witness))
assert merges == 1
assert caught and caught[0][:2] == ("and_ab", "impostor")
assert caught[0][2] == (1, 1, 1)
full = truth_table(lambda b: (b[0] & b[1]) & (1 - b[2]), N)
plain = truth_table(lambda b: b[0] & b[1], N)
assert full != plain
print("PASS: 1 merge confirmed, impostor caught at corner (1,1,1)")Nobody asks the solver to swallow the miter whole: the flow description names hashing, signatures and confirmation as separate stages.
A slow run is diagnosed first by structure: how much merged, how many candidates remain, which region resists.
Random simulation is named as a heuristic for candidates, never as the verdict: only the solver confirms.
When a run stalls, ask for the merge statistics before touching the design. A miter that merges nothing has no shared structure: check that both sides really read the same libraries and constants. A run with thousands of unconfirmed candidates near one output cone points at the genuinely different logic; that cone is where manual cut points or case splits go. Never accept a pass that skipped confirmation on any output pair.
Not yet. Agreement on vectors only proposes the pair; equivalence needs the solver to find no distinguishing input. The impostor in the worked example agrees on seven of eight corners and is still wrong.