{"abstract":"Writes past full advance the pointer and corrupt the flags.","category":"Digital logic simulation","checks":6,"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]].","evaluation_group":"w2-digital-logic-simulation-async-fifo-flags","failed_approach":"Checking the live read pointer ignores synchronizer latency, accepting writes the hardware refuses.","family":"w2-digital-logic-simulation-async-fifo-flags-overflow-protection","id":"FA-89331","implementations":{"attempt":{"sha256":"9d276088a066e1434fe3b611f0608f0000924e0176fd9f3715465575d3e35d7e","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(*args):\n    depth, ops = args\n    bits = depth.bit_length()\n    mod = 2 * depth\n    def gray(b):\n        return b ^ (b >> 1)\n    w = r = 0\n    hist_w = [0, 0]\n    hist_r = [0, 0]\n    out = []\n    acc = [0, 0]\n    for op in ops:\n        wsync, rsync = hist_w[-2], hist_r[-2]\n        top = 3 << (bits - 2)\n        full = gray(w) == gray(rsync) ^ top\n        empty = gray(r) == gray(wsync)\n        if op == 'w' and (w - r) % mod < depth:\n            w = (w + 1) % mod\n            acc[0] += 1\n        elif op == 'r' and not empty:\n            r = (r + 1) % mod\n            acc[1] += 1\n        hist_w.append(w)\n        hist_r.append(r)\n        out.append([int(full), int(empty)])\n    return [out, acc]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nfixtures = [[('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]])]]\nfor label, args, expected in fixtures[N-1]:\n    check(label, solve(*args), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"broken":{"sha256":"57d44a778a02478a54b11594f968c1f15563ae2df9d279475783e91701169fab","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(*args):\n    depth, ops = args\n    bits = depth.bit_length()\n    mod = 2 * depth\n    def gray(b):\n        return b ^ (b >> 1)\n    w = r = 0\n    hist_w = [0, 0]\n    hist_r = [0, 0]\n    out = []\n    acc = [0, 0]\n    for op in ops:\n        wsync, rsync = hist_w[-2], hist_r[-2]\n        top = 3 << (bits - 2)\n        full = gray(w) == gray(rsync) ^ top\n        empty = gray(r) == gray(wsync)\n        if op == 'w':\n            w = (w + 1) % mod\n            acc[0] += 1\n        elif op == 'r' and not empty:\n            r = (r + 1) % mod\n            acc[1] += 1\n        hist_w.append(w)\n        hist_r.append(r)\n        out.append([int(full), int(empty)])\n    return [out, acc]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nfixtures = [[('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]])]]\nfor label, args, expected in fixtures[N-1]:\n    check(label, solve(*args), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"fixed":{"sha256":"5f8a021febe1268e7cab12ccbe740b77ad45cfab825ffe164a6e6d913e69c735","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(*args):\n    depth, ops = args\n    bits = depth.bit_length()\n    mod = 2 * depth\n    def gray(b):\n        return b ^ (b >> 1)\n    w = r = 0\n    hist_w = [0, 0]\n    hist_r = [0, 0]\n    out = []\n    acc = [0, 0]\n    for op in ops:\n        wsync, rsync = hist_w[-2], hist_r[-2]\n        top = 3 << (bits - 2)\n        full = gray(w) == gray(rsync) ^ top\n        empty = gray(r) == gray(wsync)\n        if op == 'w' and not full:\n            w = (w + 1) % mod\n            acc[0] += 1\n        elif op == 'r' and not empty:\n            r = (r + 1) % mod\n            acc[1] += 1\n        hist_w.append(w)\n        hist_r.append(r)\n        out.append([int(full), int(empty)])\n    return [out, acc]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nfixtures = [[('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]])]]\nfor label, args, expected in fixtures[N-1]:\n    check(label, solve(*args), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"}},"limitations":"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.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"w2-digital-logic-simulation-async-fifo-flags-overflow-protection","generated_at":"2026-09-29T14:51:16.424735+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"Clock-domain-crossing FIFOs are simulated with synchronizer latency; flag comparisons on gray pointers are a common source of model bugs.","repair":"Accept a write only when the synchronized full flag is clear.","root_cause":"The write path does not check the full flag.","sha256":"0745edf353ed8359e5dcff68a23113ec4f1c2aee57852906cd1e2f0b4442fc65","title":"Write accepted while full · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":42.719,"exit_code":1,"observations":[{"actual":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0]],[4,0]],"check":"fill until full","expected":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0]],[4,0]],"passed":true},{"actual":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0],[0,0],[0,0],[0,1],[0,1]],[4,4]],"check":"fill then drain","expected":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0],[0,0],[0,0],[0,1],[0,1]],[4,4]],"passed":true},{"actual":[[[0,1],[0,1],[0,0],[0,1],[0,1]],[1,1]],"check":"empty flag lags writes","expected":[[[0,1],[0,1],[0,0],[0,1],[0,1]],[1,1]],"passed":true},{"actual":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0],[1,0],[1,0]],[5,1]],"check":"full flag lags reads","expected":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0],[0,0],[1,0]],[5,1]],"passed":false},{"actual":[[[0,1],[0,1],[0,0],[0,0],[0,1],[0,1],[0,0],[0,0],[0,1]],[5,4]],"check":"wrap around pointers","expected":[[[0,1],[0,1],[0,0],[0,0],[0,1],[0,1],[0,0],[0,0],[0,1]],[5,4]],"passed":true},{"actual":[[[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]],"check":"depth eight","expected":[[[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":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"fill until full\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]], \"passed\": true}, {\"check\": \"fill then drain\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]], \"passed\": true}, {\"check\": \"empty flag lags writes\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]], \"passed\": true}, {\"check\": \"full flag lags reads\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [1, 0]], [5, 1]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]], \"passed\": false}, {\"check\": \"wrap around pointers\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]], \"passed\": true}, {\"check\": \"depth eight\", \"actual\": [[[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]], \"expected\": [[[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\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":42.58,"exit_code":1,"observations":[{"actual":[[[0,1],[0,1],[0,0],[0,0],[1,0],[0,0]],[6,0]],"check":"fill until full","expected":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0]],[4,0]],"passed":false},{"actual":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0],[0,0],[0,0],[0,1],[0,1]],[4,4]],"check":"fill then drain","expected":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0],[0,0],[0,0],[0,1],[0,1]],[4,4]],"passed":true},{"actual":[[[0,1],[0,1],[0,0],[0,1],[0,1]],[1,1]],"check":"empty flag lags writes","expected":[[[0,1],[0,1],[0,0],[0,1],[0,1]],[1,1]],"passed":true},{"actual":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0],[1,0],[0,0]],[7,1]],"check":"full flag lags reads","expected":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0],[0,0],[1,0]],[5,1]],"passed":false},{"actual":[[[0,1],[0,1],[0,0],[0,0],[0,1],[0,1],[0,0],[0,0],[0,1]],[5,4]],"check":"wrap around pointers","expected":[[[0,1],[0,1],[0,0],[0,0],[0,1],[0,1],[0,0],[0,0],[0,1]],[5,4]],"passed":true},{"actual":[[[0,1],[0,1],[0,0],[0,0],[0,0],[0,0],[0,0],[0,0],[1,0],[0,0],[0,0],[0,0],[0,0],[0,0],[0,0]],[12,1]],"check":"depth eight","expected":[[[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":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"fill until full\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [0, 0]], [6, 0]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]], \"passed\": false}, {\"check\": \"fill then drain\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]], \"passed\": true}, {\"check\": \"empty flag lags writes\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]], \"passed\": true}, {\"check\": \"full flag lags reads\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [1, 0], [0, 0]], [7, 1]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]], \"passed\": false}, {\"check\": \"wrap around pointers\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]], \"passed\": true}, {\"check\": \"depth eight\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [1, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0], [0, 0]], [12, 1]], \"expected\": [[[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\": false}], \"passed\": false}\n"},"fixed":{"elapsed_ms":40.386,"exit_code":0,"observations":[{"actual":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0]],[4,0]],"check":"fill until full","expected":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0]],[4,0]],"passed":true},{"actual":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0],[0,0],[0,0],[0,1],[0,1]],[4,4]],"check":"fill then drain","expected":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0],[0,0],[0,0],[0,1],[0,1]],[4,4]],"passed":true},{"actual":[[[0,1],[0,1],[0,0],[0,1],[0,1]],[1,1]],"check":"empty flag lags writes","expected":[[[0,1],[0,1],[0,0],[0,1],[0,1]],[1,1]],"passed":true},{"actual":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0],[0,0],[1,0]],[5,1]],"check":"full flag lags reads","expected":[[[0,1],[0,1],[0,0],[0,0],[1,0],[1,0],[0,0],[1,0]],[5,1]],"passed":true},{"actual":[[[0,1],[0,1],[0,0],[0,0],[0,1],[0,1],[0,0],[0,0],[0,1]],[5,4]],"check":"wrap around pointers","expected":[[[0,1],[0,1],[0,0],[0,0],[0,1],[0,1],[0,0],[0,0],[0,1]],[5,4]],"passed":true},{"actual":[[[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]],"check":"depth eight","expected":[[[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":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"fill until full\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0]], [4, 0]], \"passed\": true}, {\"check\": \"fill then drain\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [0, 0], [0, 1], [0, 1]], [4, 4]], \"passed\": true}, {\"check\": \"empty flag lags writes\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 1], [0, 1]], [1, 1]], \"passed\": true}, {\"check\": \"full flag lags reads\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 0], [1, 0], [1, 0], [0, 0], [1, 0]], [5, 1]], \"passed\": true}, {\"check\": \"wrap around pointers\", \"actual\": [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]], \"expected\": [[[0, 1], [0, 1], [0, 0], [0, 0], [0, 1], [0, 1], [0, 0], [0, 0], [0, 1]], [5, 4]], \"passed\": true}, {\"check\": \"depth eight\", \"actual\": [[[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]], \"expected\": [[[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\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}