FAILURE MAP
← Case archive

FA-88916 / Digital logic simulation / Open access

Asynchronous reset waits for a clock edge · case 01

Asserting reset between clock edges leaves q at its old value until the next rising edge.

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

ROOT CAUSE

The reset branch is gated by the clock edge, turning an asynchronous reset into a synchronous one.

VERIFIED REPAIR

Apply reset on every sample where rst_n is 0, independent of the clock.

Unsuccessful approach: Gating reset on clock-high still ignores a reset asserted while the clock is low.

Case contract

Input: samples [clk, d, en, rst_n] at successive instants. q starts as "x". Active-low rst_n==0 forces q=0 immediately regardless of clock. Otherwise a rising clock edge (previous sample clk 0, this sample clk 1; the first sample is never an edge) with en==1 loads d. The previous clock value is tracked on every sample, including while reset is asserted. Return q after each sample.

Why this case matters

Register models in cycle simulators must distinguish asynchronous from synchronous control and detect true clock edges.

1 / The failure

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

N = 1
observations = []
def solve(samples):
    out = []
    q = 'x'
    prev = None
    for c, d, en, rst_n in samples:
        edge = prev == 0 and c == 1
        prev = c
        if rst_n == 0 and edge:
            q = 0
        elif edge and en == 1:
            q = d
        out.append(q)
    return out
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 1, 1, 1]]], ['x', 'x', 1]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0], [1, 1, 1, 1]]], ['x', 1, 0, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1], [0, 0, 1, 1]]], ['x', 1, 1, 1, 1])], [('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 0]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0], [1, 1, 1, 1], [0, 1, 1, 1]]], ['x', 1, 0, 0, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1, 1, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1, 1, 0])], [('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 1, 1, 1]]], ['x', 'x', 1]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0]]], ['x', 1, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1, 1, 1, 1, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0, 0, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1]]], ['x', 1, 1, 1])], [('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 0]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0], [1, 1, 1, 1]]], ['x', 1, 0, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0, 0, 0, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1], [0, 0, 1, 1]]], ['x', 1, 1, 1, 1])], [('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 1, 1, 1]]], ['x', 'x', 1]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0], [1, 1, 1, 1], [0, 1, 1, 1]]], ['x', 1, 0, 0, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0, 0, 0, 0, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1, 1, 0])]]
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
uninitialized flop holds x until first edge['x', 'x', 1]['x', 'x', 1]Passed
async reset between edges['x', 1, 1, 1]['x', 1, 0, 0]Failed
reset held low while clock rises['x', 0, 0, 0, 0, 1][0, 0, 0, 0, 0, 1]Failed
reset released during clock high['x', 'x', 0, 0, 0, 0]['x', 0, 0, 0, 0, 0]Failed
falling edges do not capture['x', 'x', 1, 1, 1, 0]['x', 'x', 1, 1, 1, 0]Passed
clock held high does not recapture['x', 1, 1, 1]['x', 1, 1, 1]Passed
enable low holds value['x', 1, 1, 1, 1]['x', 1, 1, 1, 1]Passed

SHA-256 / 16d57c77582782710908c73a6cf0e2cf667eef29b7fd8fac0d804636e8926c48

2 / The unsuccessful fix

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

N = 1
observations = []
def solve(samples):
    out = []
    q = 'x'
    prev = None
    for c, d, en, rst_n in samples:
        edge = prev == 0 and c == 1
        prev = c
        if rst_n == 0 and c == 1:
            q = 0
        elif edge and en == 1:
            q = d
        out.append(q)
    return out
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 1, 1, 1]]], ['x', 'x', 1]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0], [1, 1, 1, 1]]], ['x', 1, 0, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1], [0, 0, 1, 1]]], ['x', 1, 1, 1, 1])], [('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 0]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0], [1, 1, 1, 1], [0, 1, 1, 1]]], ['x', 1, 0, 0, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1, 1, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1, 1, 0])], [('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 1, 1, 1]]], ['x', 'x', 1]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0]]], ['x', 1, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1, 1, 1, 1, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0, 0, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1]]], ['x', 1, 1, 1])], [('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 0]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0], [1, 1, 1, 1]]], ['x', 1, 0, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0, 0, 0, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1], [0, 0, 1, 1]]], ['x', 1, 1, 1, 1])], [('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 1, 1, 1]]], ['x', 'x', 1]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0], [1, 1, 1, 1], [0, 1, 1, 1]]], ['x', 1, 0, 0, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0, 0, 0, 0, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1, 1, 0])]]
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
uninitialized flop holds x until first edge['x', 'x', 1]['x', 'x', 1]Passed
async reset between edges['x', 1, 0, 0]['x', 1, 0, 0]Passed
reset held low while clock rises['x', 0, 0, 0, 0, 1][0, 0, 0, 0, 0, 1]Failed
reset released during clock high['x', 'x', 0, 0, 0, 0]['x', 0, 0, 0, 0, 0]Failed
falling edges do not capture['x', 'x', 1, 1, 1, 0]['x', 'x', 1, 1, 1, 0]Passed
clock held high does not recapture['x', 1, 1, 1]['x', 1, 1, 1]Passed
enable low holds value['x', 1, 1, 1, 1]['x', 1, 1, 1, 1]Passed

SHA-256 / 665ce11977cea55560a3ed5b6591450b3b6b53657e662b14e805be7706a95ad6

3 / The verified repair

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

N = 1
observations = []
def solve(samples):
    out = []
    q = 'x'
    prev = None
    for c, d, en, rst_n in samples:
        edge = prev == 0 and c == 1
        prev = c
        if rst_n == 0:
            q = 0
        elif edge and en == 1:
            q = d
        out.append(q)
    return out
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 1, 1, 1]]], ['x', 'x', 1]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0], [1, 1, 1, 1]]], ['x', 1, 0, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1], [0, 0, 1, 1]]], ['x', 1, 1, 1, 1])], [('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 0]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0], [1, 1, 1, 1], [0, 1, 1, 1]]], ['x', 1, 0, 0, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1, 1, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1, 1, 0])], [('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 1, 1, 1]]], ['x', 'x', 1]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0]]], ['x', 1, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1, 1, 1, 1, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0, 0, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1]]], ['x', 1, 1, 1])], [('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 0]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0], [1, 1, 1, 1]]], ['x', 1, 0, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0, 0, 0, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1], [0, 0, 1, 1]]], ['x', 1, 1, 1, 1])], [('uninitialized flop holds x until first edge', [[[0, 1, 1, 1], [0, 0, 1, 1], [1, 1, 1, 1]]], ['x', 'x', 1]), ('async reset between edges', [[[0, 0, 1, 1], [1, 1, 1, 1], [1, 1, 1, 0], [1, 1, 1, 1], [0, 1, 1, 1]]], ['x', 1, 0, 0, 0]), ('reset held low while clock rises', [[[0, 0, 1, 0], [1, 1, 1, 0], [0, 1, 1, 0], [1, 1, 1, 0], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1]]], [0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1]), ('reset released during clock high', [[[0, 1, 1, 1], [0, 1, 1, 0], [1, 1, 1, 0], [1, 1, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 0, 0, 0, 0, 0]), ('falling edges do not capture', [[[1, 0, 1, 1], [0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 1, 1], [0, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 'x', 1, 1, 1, 0, 0, 0, 0, 0]), ('clock held high does not recapture', [[[0, 1, 1, 1], [1, 1, 1, 1], [1, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1]), ('enable low holds value', [[[0, 1, 1, 1], [1, 1, 1, 1], [0, 0, 0, 1], [1, 0, 0, 1], [0, 0, 1, 1], [1, 0, 1, 1]]], ['x', 1, 1, 1, 1, 0])]]
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
uninitialized flop holds x until first edge['x', 'x', 1]['x', 'x', 1]Passed
async reset between edges['x', 1, 0, 0]['x', 1, 0, 0]Passed
reset held low while clock rises[0, 0, 0, 0, 0, 1][0, 0, 0, 0, 0, 1]Passed
reset released during clock high['x', 0, 0, 0, 0, 0]['x', 0, 0, 0, 0, 0]Passed
falling edges do not capture['x', 'x', 1, 1, 1, 0]['x', 'x', 1, 1, 1, 0]Passed
clock held high does not recapture['x', 1, 1, 1]['x', 1, 1, 1]Passed
enable low holds value['x', 1, 1, 1, 1]['x', 1, 1, 1, 1]Passed

SHA-256 / b0768d8ec9763c6963ba8f4bbe67cbf2fff5fa5e9896180871f216d4384e9edb

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:12.675575+00:00.

Case digest / 216562fe3e4912e4d59a10b0160b2ee759dff840708690a8255a6f1bde01c7cb