FAILURE MAP
← Case archive

FA-89326 / Digital logic simulation / Open access

Pointer synchronizer modelled with one stage · case 01

Flags react one step early compared with a two-flop synchronizer.

Verified by executionVariant 1 · 6 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

The synchronized pointer is taken from the previous step instead of two steps back.

VERIFIED REPAIR

Use the other pointer value from two steps earlier for both flags.

Unsuccessful approach: Delaying only the write pointer leaves the full flag too optimistic.

Case contract

Input [depth, ops] with depth a power of two >= 4 and ops 'w','r','n'. Pointers are binary modulo 2*depth. Each step first computes flags from gray codes (g = b ^ (b >> 1)) using the other side's pointer as it was two steps earlier: full when gray(w) equals gray(r_sync) with its top two bits inverted, empty when gray(r) equals gray(w_sync). A write happens only if not full, a read only if not empty. Return [[full, empty] per step, [writes accepted, reads accepted]].

Why this case matters

Clock-domain-crossing FIFOs are simulated with synchronizer latency; flag comparisons on gray pointers are a common source of model bugs.

1 / The failure

Exit 1
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(*args):
    depth, ops = args
    bits = depth.bit_length()
    mod = 2 * depth
    def gray(b):
        return b ^ (b >> 1)
    w = r = 0
    hist_w = [0, 0]
    hist_r = [0, 0]
    out = []
    acc = [0, 0]
    for op in ops:
        wsync, rsync = hist_w[-1], hist_r[-1]
        top = 3 << (bits - 2)
        full = gray(w) == gray(rsync) ^ top
        empty = gray(r) == gray(wsync)
        if op == 'w' and not full:
            w = (w + 1) % mod
            acc[0] += 1
        elif op == 'r' and not empty:
            r = (r + 1) % mod
            acc[1] += 1
        hist_w.append(w)
        hist_r.append(r)
        out.append([int(full), int(empty)])
    return [out, acc]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])], [('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1]], [6, 4]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])], [('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n', 'n', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w', 'w', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0]], [6, 5]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])], [('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n', 'n', 'n', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1], [0, 1], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w', 'w', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0]], [6, 6]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])], [('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n', 'n', 'n', 'n', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1], [0, 1], [0, 1], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w', 'w', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0]], [6, 6]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])]]
for label, args, expected in fixtures[N-1]:
    check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
Boundary fixtureActualExpectedOutcome
fill until full[[[0, 1], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]][[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]]Failed
fill then drain[[[0, 1], [0, 0], [0, 0], [0, 0], [1, 0], [0, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]][[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]Failed
empty flag lags writes[[[0, 1], [0, 0], [0, 1], [0, 1], [0, 1]], [1, 1]][[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]]Failed
full flag lags reads[[[0, 1], [0, 0], [0, 0], [0, 0], [1, 0], [0, 0], [1, 0], [1, 0]], [5, 1]][[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]Failed
wrap around pointers[[[0, 1], [0, 0], [0, 0], [0, 0], [0, 1], [0, 0], [0, 0], [0, 0], [0, 1]], [5, 4]][[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]]Failed
depth eight[[[0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 0], [1, 0]], [9, 1]][[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]]Failed

SHA-256 / 31a6fbbdb7fb3637e3a0fa4979d0ce1e53e3658175e83376d9c307c48089553e

2 / The unsuccessful fix

Exit 1
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(*args):
    depth, ops = args
    bits = depth.bit_length()
    mod = 2 * depth
    def gray(b):
        return b ^ (b >> 1)
    w = r = 0
    hist_w = [0, 0]
    hist_r = [0, 0]
    out = []
    acc = [0, 0]
    for op in ops:
        wsync, rsync = hist_w[-2], hist_r[-1]
        top = 3 << (bits - 2)
        full = gray(w) == gray(rsync) ^ top
        empty = gray(r) == gray(wsync)
        if op == 'w' and not full:
            w = (w + 1) % mod
            acc[0] += 1
        elif op == 'r' and not empty:
            r = (r + 1) % mod
            acc[1] += 1
        hist_w.append(w)
        hist_r.append(r)
        out.append([int(full), int(empty)])
    return [out, acc]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])], [('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1]], [6, 4]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])], [('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n', 'n', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w', 'w', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0]], [6, 5]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])], [('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n', 'n', 'n', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1], [0, 1], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w', 'w', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0]], [6, 6]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])], [('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n', 'n', 'n', 'n', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1], [0, 1], [0, 1], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w', 'w', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0]], [6, 6]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])]]
for label, args, expected in fixtures[N-1]:
    check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
Boundary fixtureActualExpectedOutcome
fill until full[[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]][[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]]Passed
fill then drain[[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [0, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]][[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]Failed
empty flag lags writes[[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]][[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]]Passed
full flag lags reads[[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [0, 0], [1, 0], [1, 0]], [5, 1]][[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]Failed
wrap around pointers[[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]][[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]]Passed
depth eight[[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 0], [1, 0]], [9, 1]][[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]]Failed

SHA-256 / 97a631030916d8ecf4ad5b1f34baae0a41961362ba86197fb947450f11c3a2c0

3 / The verified repair

Exit 0
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(*args):
    depth, ops = args
    bits = depth.bit_length()
    mod = 2 * depth
    def gray(b):
        return b ^ (b >> 1)
    w = r = 0
    hist_w = [0, 0]
    hist_r = [0, 0]
    out = []
    acc = [0, 0]
    for op in ops:
        wsync, rsync = hist_w[-2], hist_r[-2]
        top = 3 << (bits - 2)
        full = gray(w) == gray(rsync) ^ top
        empty = gray(r) == gray(wsync)
        if op == 'w' and not full:
            w = (w + 1) % mod
            acc[0] += 1
        elif op == 'r' and not empty:
            r = (r + 1) % mod
            acc[1] += 1
        hist_w.append(w)
        hist_r.append(r)
        out.append([int(full), int(empty)])
    return [out, acc]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])], [('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1]], [6, 4]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])], [('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n', 'n', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w', 'w', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0]], [6, 5]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])], [('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n', 'n', 'n', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1], [0, 1], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w', 'w', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0]], [6, 6]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])], [('fill until full', [4, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0]], [4, 0]]), ('fill then drain', [4, ['w', 'w', 'w', 'w', 'r', 'r', 'r', 'r', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]), ('empty flag lags writes', [4, ['w', 'r', 'r', 'r', 'n', 'n', 'n', 'n', 'n']], [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1], [0, 1], [0, 1], [0, 1], [0, 1]], [1, 1]]), ('full flag lags reads', [4, ['w', 'w', 'w', 'w', 'r', 'w', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]), ('wrap around pointers', [4, ['w', 'w', 'r', 'r', 'w', 'w', 'r', 'r', 'w', 'w', 'r', 'r']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0]], [6, 6]]), ('depth eight', [8, ['w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'w', 'r', 'n', 'n', 'w', 'w']], [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]])]]
for label, args, expected in fixtures[N-1]:
    check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
Boundary fixtureActualExpectedOutcome
fill until full[[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]][[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]]Passed
fill then drain[[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]][[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]]Passed
empty flag lags writes[[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]][[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]]Passed
full flag lags reads[[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]][[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]]Passed
wrap around pointers[[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]][[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]]Passed
depth eight[[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]][[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0], [0, 0], [0, 0], [1, 0]], [9, 1]]Passed

SHA-256 / 5f8a021febe1268e7cab12ccbe740b77ad45cfab825ffe164a6e6d913e69c735

Verification & scope

A deterministic bounded teaching model of one simulator rule set; the contract is stipulated and is not a claim of conformance to any HDL standard or commercial simulator. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.

Observations recorded using Python 3.12.14 at 2026-09-29T14:51:16.223250+00:00.

Case digest / 78f2f7a889eaa468898ce0f76ac4e320e6e026fda573a516bd59a4b695651b1e