FA-89056 / Digital logic simulation / Open access
Blocking-assigned variables forget their value between steps · case 01
A variable updated only by blocking assignment restarts from its initial value every step.
ROOT CAUSE
Only queued non-blocking updates are carried into the next step.
VERIFIED REPAIR
Carry the whole working state, including blocking updates, into the next step.
Unsuccessful approach: Persisting only variables that have some non-blocking writer still loses blocking-only state.
Case contract
Input [regs, stmts, cycles]. Each clock step executes stmts [kind, lhs, op, a, b] in order (ops copy/inv/and/xor on 0/1). Blocking ('b') statements update the working state immediately; non-blocking ('nb') statements evaluate their right side at the statement against the working state and queue the update. After all statements, queued updates apply in statement order (last write wins). Every variable, blocking or not, keeps its value into the next step. Return per-step values sorted by variable name.
Why this case matters
Event-driven RTL simulation depends on the active/NBA region split; mis-scheduling produces races that do not exist in hardware.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(*args):
regs, stmts, cycles = args
regs = dict(regs)
hist = []
def ev(op, a, b, env):
if op == 'copy': return env[a]
if op == 'inv': return 1 - env[a]
if op == 'and': return env[a] & env[b]
return env[a] ^ env[b]
for _ in range(cycles):
cur = dict(regs)
nba = []
for kind, lhs, op, a, b in stmts:
v = ev(op, a, b, cur)
if kind == 'b':
cur[lhs] = v
else:
nba.append((lhs, v))
for lhs, v in nba:
cur[lhs] = v
regs.update(dict(nba))
hist.append([regs[k] for k in sorted(regs)])
return hist
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 1], [[0, 1]]), ('blocking chain inside one step', [{'a': 1, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[0, 0, 0], [1, 1, 1]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 2], [[0, 0], [1, 1]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 2], [[0, 1], [1, 0]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 3], [[0, 1, 0], [1, 0, 1], [1, 1, 0]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 1], [[0, 1, 1, 1]])], [('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 2], [[0, 1], [1, 0]]), ('blocking chain inside one step', [{'a': 0, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[1, 1, 1], [0, 0, 0]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 3], [[0, 0], [1, 1], [0, 0]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 3], [[0, 1], [1, 0], [0, 1]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 4], [[0, 1, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 2], [[0, 1, 1, 1], [0, 1, 0, 1]])], [('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 3], [[0, 1], [1, 0], [0, 1]]), ('blocking chain inside one step', [{'a': 1, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[0, 0, 0], [1, 1, 1]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 4], [[0, 0], [1, 1], [0, 0], [1, 1]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 4], [[0, 1], [1, 0], [0, 1], [1, 0]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 5], [[0, 1, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1], [0, 1, 1]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 3], [[0, 1, 1, 1], [0, 1, 0, 1], [0, 1, 0, 1]])], [('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 4], [[0, 1], [1, 0], [0, 1], [1, 0]]), ('blocking chain inside one step', [{'a': 0, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[1, 1, 1], [0, 0, 0]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 5], [[0, 0], [1, 1], [0, 0], [1, 1], [0, 0]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 5], [[0, 1], [1, 0], [0, 1], [1, 0], [0, 1]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 6], [[0, 1, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1], [0, 1, 1], [0, 0, 1]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 4], [[0, 1, 1, 1], [0, 1, 0, 1], [0, 1, 0, 1], [0, 1, 0, 1]])], [('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 5], [[0, 1], [1, 0], [0, 1], [1, 0], [0, 1]]), ('blocking chain inside one step', [{'a': 1, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[0, 0, 0], [1, 1, 1]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 6], [[0, 0], [1, 1], [0, 0], [1, 1], [0, 0], [1, 1]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 6], [[0, 1], [1, 0], [0, 1], [1, 0], [0, 1], [1, 0]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 7], [[0, 1, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1], [0, 1, 1], [0, 0, 1], [1, 0, 0]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 5], [[0, 1, 1, 1], [0, 1, 0, 1], [0, 1, 0, 1], [0, 1, 0, 1], [0, 1, 0, 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 fixture | Actual | Expected | Outcome |
|---|---|---|---|
| non-blocking swap | [[0, 1]] | [[0, 1]] | Passed |
| blocking chain inside one step | [[0, 0, 0], [1, 0, 0]] | [[0, 0, 0], [1, 1, 1]] | Failed |
| later non-blocking write wins | [[0, 0], [1, 1]] | [[0, 0], [1, 1]] | Passed |
| blocking temp persists across cycles | [[0, 0], [0, 0]] | [[0, 1], [1, 0]] | Failed |
| shift register with non-blocking | [[0, 1, 0], [1, 0, 1], [1, 1, 0]] | [[0, 1, 0], [1, 0, 1], [1, 1, 0]] | Passed |
| non-blocking reads blocking result | [[0, 1, 0, 1]] | [[0, 1, 1, 1]] | Failed |
SHA-256 / ffa2c6452b298388d18b112c763f35deba7d6b6cbdeb1f5eaf595307bce97326
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(*args):
regs, stmts, cycles = args
regs = dict(regs)
hist = []
def ev(op, a, b, env):
if op == 'copy': return env[a]
if op == 'inv': return 1 - env[a]
if op == 'and': return env[a] & env[b]
return env[a] ^ env[b]
for _ in range(cycles):
cur = dict(regs)
nba = []
for kind, lhs, op, a, b in stmts:
v = ev(op, a, b, cur)
if kind == 'b':
cur[lhs] = v
else:
nba.append((lhs, v))
for lhs, v in nba:
cur[lhs] = v
regs.update({k: v for k, v in cur.items() if any(s[1] == k and s[0] == 'nb' for s in stmts)})
hist.append([regs[k] for k in sorted(regs)])
return hist
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 1], [[0, 1]]), ('blocking chain inside one step', [{'a': 1, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[0, 0, 0], [1, 1, 1]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 2], [[0, 0], [1, 1]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 2], [[0, 1], [1, 0]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 3], [[0, 1, 0], [1, 0, 1], [1, 1, 0]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 1], [[0, 1, 1, 1]])], [('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 2], [[0, 1], [1, 0]]), ('blocking chain inside one step', [{'a': 0, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[1, 1, 1], [0, 0, 0]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 3], [[0, 0], [1, 1], [0, 0]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 3], [[0, 1], [1, 0], [0, 1]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 4], [[0, 1, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 2], [[0, 1, 1, 1], [0, 1, 0, 1]])], [('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 3], [[0, 1], [1, 0], [0, 1]]), ('blocking chain inside one step', [{'a': 1, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[0, 0, 0], [1, 1, 1]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 4], [[0, 0], [1, 1], [0, 0], [1, 1]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 4], [[0, 1], [1, 0], [0, 1], [1, 0]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 5], [[0, 1, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1], [0, 1, 1]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 3], [[0, 1, 1, 1], [0, 1, 0, 1], [0, 1, 0, 1]])], [('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 4], [[0, 1], [1, 0], [0, 1], [1, 0]]), ('blocking chain inside one step', [{'a': 0, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[1, 1, 1], [0, 0, 0]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 5], [[0, 0], [1, 1], [0, 0], [1, 1], [0, 0]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 5], [[0, 1], [1, 0], [0, 1], [1, 0], [0, 1]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 6], [[0, 1, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1], [0, 1, 1], [0, 0, 1]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 4], [[0, 1, 1, 1], [0, 1, 0, 1], [0, 1, 0, 1], [0, 1, 0, 1]])], [('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 5], [[0, 1], [1, 0], [0, 1], [1, 0], [0, 1]]), ('blocking chain inside one step', [{'a': 1, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[0, 0, 0], [1, 1, 1]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 6], [[0, 0], [1, 1], [0, 0], [1, 1], [0, 0], [1, 1]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 6], [[0, 1], [1, 0], [0, 1], [1, 0], [0, 1], [1, 0]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 7], [[0, 1, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1], [0, 1, 1], [0, 0, 1], [1, 0, 0]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 5], [[0, 1, 1, 1], [0, 1, 0, 1], [0, 1, 0, 1], [0, 1, 0, 1], [0, 1, 0, 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 fixture | Actual | Expected | Outcome |
|---|---|---|---|
| non-blocking swap | [[0, 1]] | [[0, 1]] | Passed |
| blocking chain inside one step | [[0, 0, 0], [1, 0, 0]] | [[0, 0, 0], [1, 1, 1]] | Failed |
| later non-blocking write wins | [[0, 0], [1, 1]] | [[0, 0], [1, 1]] | Passed |
| blocking temp persists across cycles | [[0, 0], [0, 0]] | [[0, 1], [1, 0]] | Failed |
| shift register with non-blocking | [[0, 1, 0], [1, 0, 1], [1, 1, 0]] | [[0, 1, 0], [1, 0, 1], [1, 1, 0]] | Passed |
| non-blocking reads blocking result | [[0, 1, 0, 1]] | [[0, 1, 1, 1]] | Failed |
SHA-256 / b24198aecb7f6d9182adfd9956577b517d8c8f63e1137b639f5c0f4ac292f042
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(*args):
regs, stmts, cycles = args
regs = dict(regs)
hist = []
def ev(op, a, b, env):
if op == 'copy': return env[a]
if op == 'inv': return 1 - env[a]
if op == 'and': return env[a] & env[b]
return env[a] ^ env[b]
for _ in range(cycles):
cur = dict(regs)
nba = []
for kind, lhs, op, a, b in stmts:
v = ev(op, a, b, cur)
if kind == 'b':
cur[lhs] = v
else:
nba.append((lhs, v))
for lhs, v in nba:
cur[lhs] = v
regs = cur
hist.append([regs[k] for k in sorted(regs)])
return hist
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 1], [[0, 1]]), ('blocking chain inside one step', [{'a': 1, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[0, 0, 0], [1, 1, 1]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 2], [[0, 0], [1, 1]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 2], [[0, 1], [1, 0]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 3], [[0, 1, 0], [1, 0, 1], [1, 1, 0]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 1], [[0, 1, 1, 1]])], [('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 2], [[0, 1], [1, 0]]), ('blocking chain inside one step', [{'a': 0, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[1, 1, 1], [0, 0, 0]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 3], [[0, 0], [1, 1], [0, 0]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 3], [[0, 1], [1, 0], [0, 1]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 4], [[0, 1, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 2], [[0, 1, 1, 1], [0, 1, 0, 1]])], [('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 3], [[0, 1], [1, 0], [0, 1]]), ('blocking chain inside one step', [{'a': 1, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[0, 0, 0], [1, 1, 1]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 4], [[0, 0], [1, 1], [0, 0], [1, 1]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 4], [[0, 1], [1, 0], [0, 1], [1, 0]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 5], [[0, 1, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1], [0, 1, 1]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 3], [[0, 1, 1, 1], [0, 1, 0, 1], [0, 1, 0, 1]])], [('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 4], [[0, 1], [1, 0], [0, 1], [1, 0]]), ('blocking chain inside one step', [{'a': 0, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[1, 1, 1], [0, 0, 0]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 5], [[0, 0], [1, 1], [0, 0], [1, 1], [0, 0]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 5], [[0, 1], [1, 0], [0, 1], [1, 0], [0, 1]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 6], [[0, 1, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1], [0, 1, 1], [0, 0, 1]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 4], [[0, 1, 1, 1], [0, 1, 0, 1], [0, 1, 0, 1], [0, 1, 0, 1]])], [('non-blocking swap', [{'a': 1, 'b': 0}, [['nb', 'a', 'copy', 'b', None], ['nb', 'b', 'copy', 'a', None]], 5], [[0, 1], [1, 0], [0, 1], [1, 0], [0, 1]]), ('blocking chain inside one step', [{'a': 1, 't': 0, 'u': 0}, [['b', 't', 'inv', 'a', None], ['b', 'u', 'copy', 't', None], ['nb', 'a', 'copy', 'u', None]], 2], [[0, 0, 0], [1, 1, 1]]), ('later non-blocking write wins', [{'a': 1, 'c': 0}, [['nb', 'c', 'copy', 'a', None], ['nb', 'c', 'inv', 'a', None], ['nb', 'a', 'inv', 'a', None]], 6], [[0, 0], [1, 1], [0, 0], [1, 1], [0, 0], [1, 1]]), ('blocking temp persists across cycles', [{'t': 0, 'c': 0}, [['nb', 'c', 'copy', 't', None], ['b', 't', 'inv', 't', None]], 6], [[0, 1], [1, 0], [0, 1], [1, 0], [0, 1], [1, 0]]), ('shift register with non-blocking', [{'s0': 1, 's1': 0, 's2': 0}, [['nb', 's1', 'copy', 's0', None], ['nb', 's2', 'copy', 's1', None], ['nb', 's0', 'xor', 's2', 's1']], 7], [[0, 1, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1], [0, 1, 1], [0, 0, 1], [1, 0, 0]]), ('non-blocking reads blocking result', [{'a': 1, 'b': 1, 'y': 0, 'm': 0}, [['b', 'm', 'and', 'a', 'b'], ['nb', 'y', 'xor', 'm', 'y'], ['nb', 'a', 'inv', 'b', None]], 5], [[0, 1, 1, 1], [0, 1, 0, 1], [0, 1, 0, 1], [0, 1, 0, 1], [0, 1, 0, 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 fixture | Actual | Expected | Outcome |
|---|---|---|---|
| non-blocking swap | [[0, 1]] | [[0, 1]] | Passed |
| blocking chain inside one step | [[0, 0, 0], [1, 1, 1]] | [[0, 0, 0], [1, 1, 1]] | Passed |
| later non-blocking write wins | [[0, 0], [1, 1]] | [[0, 0], [1, 1]] | Passed |
| blocking temp persists across cycles | [[0, 1], [1, 0]] | [[0, 1], [1, 0]] | Passed |
| shift register with non-blocking | [[0, 1, 0], [1, 0, 1], [1, 1, 0]] | [[0, 1, 0], [1, 0, 1], [1, 1, 0]] | Passed |
| non-blocking reads blocking result | [[0, 1, 1, 1]] | [[0, 1, 1, 1]] | Passed |
SHA-256 / c29668fd1d44990c90b555e66a03d99e9cc3218fd264d94680c45001e60254b3
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:13.961836+00:00.
Case digest / 3e59779f45bd0d91d7dc7d625457a32f823dc188aeadbff180b6f8b1dd253a57