Why it matters

The comparator fires at 2 a.m. with a 40-signal trace. Three different mornings teach three different endings: a dropped carry term in the new adder, a signed-versus-unsigned compare nobody aligned, and a constant tied high on one side of the setup. Only one of the three is a design bug, but all three look identical until they are read. This lesson is the reading discipline.

This lesson has one job: turn a failing miter into a diagnosis of real difference versus setup difference, with the smallest input that still shows it.

The core idea

Read the trace in four steps. First, find the earliest failing cycle: everything after it is effect, not cause. Second, name the output bits that differ and trace them back to one cone: the divergence starts where the two cones first compute different values. Third, minimise the input: clear bits one by one while the mismatch persists, until removing any remaining bit hides it. Fourth, classify: a real difference survives aligned constants, widths and signedness; a setup difference vanishes the moment the setup is fixed.

Three mismatch shapes cover most mornings. A carry corner differs on one output bit for a few complementary inputs: real logic difference. A signed-versus-unsigned compare differs on exactly the inputs where the top bit is set: interpretation difference, fixed by declaring signedness once. A constant tie-off differs on every input: setup difference, fixed in the harness, and the fastest to check, so check it first.

# not-run: illustrative trace, not executable here
case A (carry corner): a=0101 b=1010 cin=1 -> ref 10000 (16), dut 00000 (0)
  differs: bit 4 only (the low four bits are 0000 on both) | set input bits needed: all five | verdict: real
case B (signed compare):  a=1001 vs bound 0111 -> ref LO, dut HI
  differs: 1-bit result for all inputs with top bit set | verdict: setup (signedness)
case C (tie-off): const TEST=1 on ref, 0 on dut -> outputs differ on every vector
  differs: all bits, all inputs | verdict: setup (align the tie, rerun)

Worked example: minimising a counterexample

The helper below takes a mismatch predicate and clears input bits one at a time while the mismatch persists. For the carry corner the predicate is not written by hand: it builds the two sums from a ripple adder and a lookahead adder with the longest carry term dropped, and asks whether they differ. Every set bit survives minimisation, which is the signature of a corner: the mismatch needs all of them, so five bits (four operand bits and the carry in) is the smallest input. On the tie-off predicate the result is the empty input, which is the signature of a setup difference: no design input is needed. An over-minimiser that clears bits without re-checking is also included: its result no longer shows the mismatch, and the acceptance check refuses it:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60

def lookahead(a, b, cin, bug):
    g = [((a >> i) & (b >> i)) & 1 for i in range(4)]
    p = [((a ^ b) >> i) & 1 for i in range(4)]
    c1 = g[0] | (p[0] & cin)
    c2 = g[1] | (p[1] & g[0]) | (p[1] & p[0] & cin)
    c3 = g[2] | (p[2] & g[1]) | (p[2] & p[1] & g[0]) | (p[2] & p[1] & p[0] & cin)
    c4 = g[3] | (p[3] & g[2]) | (p[3] & p[2] & g[1]) | (p[3] & p[2] & p[1] & g[0])
    if not bug:
        c4 |= p[3] & p[2] & p[1] & p[0] & cin
    c = [cin, c1, c2, c3]
    s = sum((p[i] ^ c[i]) << i for i in range(4))
    return (c4 << 4) | s

def decode(bits):
    a = sum(1 << i for i in range(4) if "a%d" % i in bits)
    b = sum(1 << i for i in range(4) if "b%d" % i in bits)
    return a, b, 1 if "cin" in bits else 0

def carry_corner(bits):
    a, b, cin = decode(bits)
    return lookahead(a, b, cin, True) != a + b + cin

def out(bits, test):
    return (1 if "a0" in bits else 0) ^ test

def tie_off(bits):
    return out(bits, 1) != out(bits, 0)

def minimise(pred, start):
    keep = set(start)
    assert pred(keep), "start must show the mismatch"
    for b in sorted(start):
        trial = keep - {b}
        if pred(trial):
            keep = trial
    return keep

def over_minimise(start, drop):
    return set(start) - set(drop)

def accept(pred, result):
    if not pred(result):
        raise ValueError("over-minimised: the mismatch is gone")
    return result

corner = {"a0", "a2", "b1", "b3", "cin"}
m1 = minimise(carry_corner, corner)
assert m1 == corner and len(m1) == 5
assert not any(carry_corner(corner - {b}) for b in corner)
m2 = minimise(tie_off, {"a0", "a1", "b2", "cin"})
assert m2 == set()
bad = over_minimise(m1, {"a0", "cin"})
assert not carry_corner(bad)
try:
    accept(carry_corner, bad)
    raise SystemExit("over-minimiser not caught")
except ValueError:
    pass
assert accept(carry_corner, m1) == m1
print("PASS: corner keeps 5 bits; setup difference needs none; over-minimiser refused")

What the review looks for

• Every failing miter ends in a written diagnosis: earliest cycle, differing bits, responsible cone, real or setup.

• Setup suspects are checked first: constants, widths, signedness, tie-offs, mode selects.

• The minimised input is replayed in simulation on both sides before any RTL is touched.

Verify and debug

Keep a triage tree at the review: all-inputs-differ points at setup, top-bit-only points at signedness, single-bit-corner points at logic. File each mismatch under one leaf with its minimised vector. A mismatch that fits no leaf is the interesting one: escalate it, do not average it away.

Related topics

• Constants, Don't-Cares and Constrained Equivalence

• Next: Product Machine and State Correspondence

• Synthesis: Reading a Failure

• Synthesis: A Netlist Fails Equivalence

• Hardware Debug: Equivalence Failures