The netlist renames half the registers and duplicates the other half across two clock-gating styles. Name matching pairs a third of the state; the rest is reported unmapped, and the run stops. The engineer who classifies the remainder by structure and function gets the pass; the one who waives it gets the escape. This lesson is the classification discipline.
This lesson has one job: find correspondence in three passes and give every unmapped point a named cause.
Key points are the compared state and output cut points. Correspondence is attempted in order. Name matching pairs registers whose hierarchical names survive synthesis. Structural matching pairs registers with identical fan-in cones up to renaming. Functional matching proves two differently named, differently structured registers always hold equal values, which is the expensive pass and is spent only where the cheaper ones fail.
Whatever remains is unmapped, and unmapped has exactly three causes. A design change adds or removes real state: re-verify the change, do not waive it. A transformation duplicates or merges state: retiming splits one flop into two, gating adds enables, and these points belong under sequential methods. A setup error drops a point: a black box with the wrong boundary, a renamed hierarchy the name pass could not see, or a constant that optimised a flop away.
The matcher below tries name, then cone signature, then exhaustive functional check over the reachable input space, recording which strategy paired each point. The clean run pairs everything by name. An injected renamed register misses the name pass and is recovered by its cone signature; an injected transformed register needs the functional pass. Unmapped leftovers are listed with their classifications:
import itertools
def match_points(rtl, gate):
pairs, used = {}, set()
for n, cone, fn in rtl:
if n in [g[0] for g in gate] and n not in used:
pairs[n] = ("name", n)
used.add(n)
for n, cone, fn in rtl:
if n in pairs:
continue
for gn, gcone, gfn in gate:
if gn in used:
continue
if gcone == cone:
pairs[n] = ("structure", gn)
used.add(gn)
break
for n, cone, fn in rtl:
if n in pairs:
continue
for gn, gcone, gfn in gate:
if gn in used:
continue
if all(fn(b) == gfn(b) for b in itertools.product([0, 1], repeat=2)):
pairs[n] = ("function", gn)
used.add(gn)
break
unmapped = [g[0] for g in gate if g[0] not in used]
missing = [n for n, _, _ in rtl if n not in pairs]
return pairs, unmapped, missing
RTL = [("a", "c1", lambda b: b[0] & b[1]),
("b", "c2", lambda b: b[0] | b[1]),
("c", "c3", lambda b: b[0] ^ b[1])]
GATE = [("a", "c1", lambda b: b[0] & b[1]),
("b_ren", "c2", lambda b: b[0] | b[1]),
("c_dup", "c9", lambda b: b[0] ^ b[1])]
pairs, unmapped, missing = match_points(RTL, GATE)
assert pairs["a"] == ("name", "a")
assert pairs["b"] == ("structure", "b_ren")
assert pairs["c"] == ("function", "c_dup")
assert unmapped == [] and missing == []
GATE_X = GATE + [("extra_flop", "c0", lambda b: 0)]
_, unmapped2, _ = match_points(RTL, GATE_X)
assert unmapped2 == ["extra_flop"]
print("PASS: name, structure, function pair all points; extra reported")The report lists per-point strategy: how many paired by name, by structure, by function.
Function-matched points carry the proof obligation: the equivalence that justifies treating them as one point.
Every unmapped point carries one of the three classifications with evidence, and transformation artefacts point at their sequential proof.
Rename a register deliberately and confirm the structure pass recovers it; duplicate a cone and confirm the function pass recovers it; add a real extra flop and confirm it stays unmapped. A matcher that pairs everything by name on a synthesised netlist is not matching: it is skipping the hard passes. Watch the strategy counts across releases: a sudden move from name to function matching means the synthesis setup changed.
The proof that justifies the pairing: the functional check that showed them always equal, and why the cheaper passes missed them, usually a rename plus a resynthesis of the cone.