A netlist passes against the RTL on Friday and the tester finds a flop that never resets on Monday. The comparison tied reset to the value the synthesis script declared, while the tester released it the other way, so the two models agreed with each other and the silicon, driven by the tester, did not. Every assumption below has a story like that: a pass that was true under the setup and false outside it.
This lesson has one job: state the four assumptions a gate-level pass rests on, and the false pass or false fail each one produces when broken.
One-to-one logic equivalence assumes a correspondence between every sequential element: same encoding, so each RTL flop has exactly one gate-level partner holding the same value in the same cycle. It assumes scan and test logic disabled, so the compared paths are the mission paths. It assumes consistent constants and black boxes: tie-offs, parameter values and undriven-box behaviour identical on both sides. And it assumes the same reset: both sides leave the same values from the same sequence. Retiming and some clock gating break the first assumption structurally, which is why they need sequential methods or dedicated modes rather than the plain comparison.
Assumption | Broken how | False result |
|---|---|---|
One-to-one state, same encoding | Retimed or recoded netlist | False fail: registers match nowhere on a correct design |
Scan and test disabled | Scan left enabled on one side | False pass or false fail: test paths compared instead of mission paths |
Consistent constants and black boxes | Tie-off differs between setups, or a box is abstracted differently per side | False fail on every vector, or false pass if the differing constant masks a bug or the setup forces the box outputs to agree |
Same reset | Different reset values or sequences | False fail in early cycles, or false pass if reset masks the divergence |
The script below models the first assumption as a checker over two flop-name lists. It pairs by name, reports unmapped and extra registers, and flags width mismatches. The clean pair passes. Then an injected extra gate-level register with no RTL partner is reported as unmapped, proving the checker can fail:
def check_mapping(rtl, gate):
rtl_names = {n for n, w in rtl}
gate_names = {n for n, w in gate}
rtl_w = dict(rtl)
gate_w = dict(gate)
unmapped = sorted(gate_names - rtl_names)
missing = sorted(rtl_names - gate_names)
widths = sorted(n for n in rtl_names & gate_names if rtl_w[n] != gate_w[n])
return unmapped, missing, widths
RTL = [("ctrl", 8), ("status", 2), ("data", 8), ("cnt", 4)]
GATE = [("ctrl", 8), ("status", 2), ("data", 8), ("cnt", 4)]
assert check_mapping(RTL, GATE) == ([], [], [])
GATE_X = GATE + [("scan_shadow", 1)]
u, m, w = check_mapping(RTL, GATE_X)
assert u == ["scan_shadow"] and m == [] and w == []
GATE_W = [("ctrl", 8), ("status", 2), ("data", 7), ("cnt", 4)]
u2, m2, w2 = check_mapping(RTL, GATE_W)
assert w2 == ["data"]
print("PASS: clean pair maps; extra register and width change reported")The result names all four assumptions with their concrete values: which scan mode, which constants, which reset sequence.
Retimed or recoded blocks are absent from the one-to-one run: they appear under sequential equivalence instead.
Unmapped registers are classified, never waived silently: design change, transformation artefact, or setup error.
Rerun the comparison once per assumption flipped: scan enabled, one constant changed, a shorter reset. Each run must fail or be explained; a run that still passes under a broken assumption is not checking what you think. Keep the assumption list beside the verdict in the signoff, not in the script header.
Constants and tie-offs: a setup difference affects every vector, while a logic difference is usually confined to some corner. Align the constants and rerun before reading any cone.