A revised block answers one cycle later than the golden model. The miter compares them sample by sample and fails on every cycle, including the cycles where both are correct. The fix is an alignment delay in the harness, but the fix itself can lie: align a constant-output design by the wrong delay and it still passes, because a flat line matches itself at any shift. This lesson shows both failures and the two-property discipline that catches them.
This lesson has one job: align latencies so the comparison is meaningful, and prove the alignment rather than trusting it.
Sequential comparison needs three statements, not one. First, the golden latency property: the reference answers exactly L cycles after the stimulus. Second, the revised latency property: the new block answers exactly M cycles after the stimulus. Third, the aligned comparison: golden delayed by the difference agrees with the revised output, compared only after both pipelines have filled and both sides have left reset.
Comparing before the defined point invites two symmetric mistakes. An alignment that is wrong by construction fails everywhere and is easy to spot. An alignment that is wrong but unnoticed passes on uninteresting stimulus, flat lines and idle cycles, and is dangerous. The latency properties exist to rule out the second mistake: they pin L and M independently of the comparison.
Reset and initial state belong to the same discipline. The miter starts both sides from the same reset step and compares equivalence from reset, so it says nothing about arbitrary power-up contents. The model is two-state: a register without a reset is an arbitrary 0 or 1, and a difference between two descriptions that only shows as an unknown in simulation is invisible to it. What the comparison can show is a reset-value difference, which appears only in the first cycles; the second example below shows it.
The script models a block that answers a pulse. The golden reference answers one cycle after the stimulus, the revised block two cycles after. Comparing the revised output against the golden delayed by one is the correct alignment and passes on every stimulus. Aligning by two fails on six of the nine compared cycles. And on an all-idle stimulus even the wrong alignment passes, which is exactly the trap: the passing verdict says nothing without an active stimulus and a separately asserted latency:
def run(lat, stim):
out = [0] * lat + [s for s in stim]
return out
def compare(rev, gold, delay, cycles, skip):
bad = []
for t in range(cycles):
g = gold[t - delay] if t - delay >= 0 else 0
if t >= skip and rev[t] != g:
bad.append(t)
return bad
stim = [0, 1, 0, 0, 1, 1, 0, 1, 0, 0, 0, 0]
gold = run(1, stim)
rev = run(2, stim)
assert compare(rev, gold, 1, 12, 3) == []
assert len(compare(rev, gold, 2, 12, 3)) == 6
idle_gold = run(1, [0] * 12)
idle_rev = run(2, [0] * 12)
assert compare(idle_rev, idle_gold, 2, 12, 3) == []
assert compare(idle_rev, idle_gold, 5, 12, 3) == []
assert gold[2] == 1 and rev[3] == 1
print("PASS: delay-by-1 clean; delay-by-2 fails active, passes idle")The last two asserts are the latency evidence in miniature: the golden pulse of cycle 1 appears at cycle 2, the revised at cycle 3. Without those two facts the idle pass would be worthless. In a real harness the same facts are cover properties: a pulse in, the answer out exactly L cycles later, witnessed.
The second script adds a reset-value mismatch: the revised block resets its output register to 1 where the golden one resets to 0. With the correct alignment the comparison fails only in the first cycles, 0 and 1 in this model, and is clean from the defined point on; a separate reset-value check at cycle 0 catches the cause directly, and the same comparison started late would never see it:
def run_reset(lat, stim, reset_value):
return [reset_value] * lat + list(stim)
def compare(rev, gold, delay, cycles, skip):
bad = []
for t in range(cycles):
g = gold[t - delay] if t - delay >= 0 else 0
if t >= skip and rev[t] != g:
bad.append(t)
return bad
stim = [0, 1, 0, 0, 1, 1, 0, 1, 0, 0, 0, 0]
gold = run_reset(1, stim, 0)
good_rev = run_reset(2, stim, 0)
bad_rev = run_reset(2, stim, 1)
assert compare(good_rev, gold, 1, 12, 0) == []
assert compare(bad_rev, gold, 1, 12, 0) == [0, 1]
assert compare(bad_rev, gold, 1, 12, 2) == []
assert bad_rev[0] != gold[0] and good_rev[0] == gold[0]
print("PASS: reset-value mismatch shows only in cycles 0 to 1; late comparison misses it")The comparison names its alignment delay and its start cycle; nothing before the fill point is compared.
Each side has its own latency property or cover, proved independently of the comparison.
Reset values are defined for both sides: comparison starts after both have left reset, and the first cycles carry a reset-value check instead.
Shift the alignment by one in each direction and confirm the comparison fails on active stimulus: an alignment nobody can break is not constraining anything. Then run idle-only stimulus and confirm the latency covers still reach: if they do not, the pass rests on flat lines. A mismatch confined to the first cycles after reset is a reset-value difference until proven otherwise; check both reset values before touching the alignment.
Nothing yet. The comparison may be passing on idle cycles. Reach the latency cover with active stimulus first; only then does the agreement mean the blocks match on real traffic.