FA-89231 / Digital logic simulation / Open access

Agreeing floating inputs pass through an unknown select · case 01

Two candidate inputs both at 'z' produce 'z' instead of 'x'.

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

ROOT CAUSE

Agreement is accepted for any value, including z.

VERIFIED REPAIR

Only agreeing definite values (0 or 1) survive an unknown select.

Unsuccessful approach: Excluding only 'x' still lets 'z' through.

Case contract

Input [kind, sel, data]: sel is MSB-first over 0/1/x/z; an x or z select bit makes both values of that bit candidates. mux: the output is the common value of all candidate data inputs if they agree and are 0 or 1, else 'x'. dec: data[0] is the enable; enable 0 gives all '0'; otherwise candidate lines are '1' only when there is a single candidate and the enable is 1, else 'x'; non-candidate lines are '0'.

Why this case matters

Unknown-select pessimism rules in RTL simulation decide whether X on a control input corrupts datapath outputs.

1 / The failure

Exit 1

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

N = 1
observations = []
def solve(*args):
    kind, sel, data = args
    cands = [0]
    for s in sel:
        if s in '01':
            cands = [c * 2 + int(s) for c in cands]
        else:
            cands = [c * 2 + b for c in cands for b in (0, 1)]
    if kind == 'mux':
        vals = sorted({data[c] for c in cands})
        return vals[0] if len(vals) == 1 else 'x'
    en = data[0]
    out = []
    for i in range(2 ** len(sel)):
        if en == '0':
            out.append('0')
        elif i in cands and (len(cands) > 1 or en != '1'):
            out.append('x')
        elif i in cands:
            out.append('1')
        else:
            out.append('0')
    return out
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x1', ['0', '1', '0', '1']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '10', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '01', ['x']], ['0', 'x', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '1', '0'])], [('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x0', ['1', '0', '1', '0']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '01', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '00', ['x']], ['x', '0', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '1', '0'])], [('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x1', ['0', '1', '0', '1']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '10', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '01', ['x']], ['0', 'x', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '1', '0'])], [('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x0', ['1', '0', '1', '0']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '01', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '00', ['x']], ['x', '0', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '1', '0'])], [('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x1', ['0', '1', '0', '1']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '10', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '01', ['x']], ['0', 'x', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '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 fixture	Actual	Expected	Outcome
mux unknown select differing data	`x`	`x`	Passed
mux unknown select agreeing data	`1`	`1`	Passed
mux4 unknown low select bit	`1`	`1`	Passed
mux4 unknown high select bit	`1`	`1`	Passed
mux unknown select floating data	`z`	`x`	Failed
mux4 known select	`1`	`1`	Passed
decoder unknown select bit	`['0', '0', 'x', 'x']`	`['0', '0', 'x', 'x']`	Passed
decoder unknown enable	`['0', 'x', '0', '0']`	`['0', 'x', '0', '0']`	Passed
decoder enabled	`['0', '0', '1', '0']`	`['0', '0', '1', '0']`	Passed

SHA-256 / 00850e15b02b083b1bd1d0aef0377716912c6987a6c5a4eac13f0435db9427bb

2 / The unsuccessful fix

Exit 1

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

N = 1
observations = []
def solve(*args):
    kind, sel, data = args
    cands = [0]
    for s in sel:
        if s in '01':
            cands = [c * 2 + int(s) for c in cands]
        else:
            cands = [c * 2 + b for c in cands for b in (0, 1)]
    if kind == 'mux':
        vals = sorted({data[c] for c in cands})
        return vals[0] if len(vals) == 1 and vals[0] != 'x' else 'x'
    en = data[0]
    out = []
    for i in range(2 ** len(sel)):
        if en == '0':
            out.append('0')
        elif i in cands and (len(cands) > 1 or en != '1'):
            out.append('x')
        elif i in cands:
            out.append('1')
        else:
            out.append('0')
    return out
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x1', ['0', '1', '0', '1']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '10', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '01', ['x']], ['0', 'x', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '1', '0'])], [('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x0', ['1', '0', '1', '0']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '01', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '00', ['x']], ['x', '0', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '1', '0'])], [('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x1', ['0', '1', '0', '1']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '10', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '01', ['x']], ['0', 'x', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '1', '0'])], [('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x0', ['1', '0', '1', '0']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '01', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '00', ['x']], ['x', '0', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '1', '0'])], [('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x1', ['0', '1', '0', '1']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '10', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '01', ['x']], ['0', 'x', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '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 fixture	Actual	Expected	Outcome
mux unknown select differing data	`x`	`x`	Passed
mux unknown select agreeing data	`1`	`1`	Passed
mux4 unknown low select bit	`1`	`1`	Passed
mux4 unknown high select bit	`1`	`1`	Passed
mux unknown select floating data	`z`	`x`	Failed
mux4 known select	`1`	`1`	Passed
decoder unknown select bit	`['0', '0', 'x', 'x']`	`['0', '0', 'x', 'x']`	Passed
decoder unknown enable	`['0', 'x', '0', '0']`	`['0', 'x', '0', '0']`	Passed
decoder enabled	`['0', '0', '1', '0']`	`['0', '0', '1', '0']`	Passed

SHA-256 / 0a08bce2bd9b7c5fa4a58a8724fad68b02554463d143e6a0ed7db795eeecd067

3 / The verified repair

Exit 0

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

N = 1
observations = []
def solve(*args):
    kind, sel, data = args
    cands = [0]
    for s in sel:
        if s in '01':
            cands = [c * 2 + int(s) for c in cands]
        else:
            cands = [c * 2 + b for c in cands for b in (0, 1)]
    if kind == 'mux':
        vals = sorted({data[c] for c in cands})
        return vals[0] if len(vals) == 1 and vals[0] in '01' else 'x'
    en = data[0]
    out = []
    for i in range(2 ** len(sel)):
        if en == '0':
            out.append('0')
        elif i in cands and (len(cands) > 1 or en != '1'):
            out.append('x')
        elif i in cands:
            out.append('1')
        else:
            out.append('0')
    return out
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x1', ['0', '1', '0', '1']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '10', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '01', ['x']], ['0', 'x', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '1', '0'])], [('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x0', ['1', '0', '1', '0']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '01', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '00', ['x']], ['x', '0', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '1', '0'])], [('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x1', ['0', '1', '0', '1']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '10', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '01', ['x']], ['0', 'x', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '1', '0'])], [('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x0', ['1', '0', '1', '0']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '01', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '00', ['x']], ['x', '0', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '1', '0'])], [('mux unknown select differing data', ['mux', 'x', ['0', '1']], 'x'), ('mux unknown select agreeing data', ['mux', 'x', ['1', '1']], '1'), ('mux4 unknown low select bit', ['mux', '1x', ['0', '1', '1', '1']], '1'), ('mux4 unknown high select bit', ['mux', 'x1', ['0', '1', '0', '1']], '1'), ('mux unknown select floating data', ['mux', 'z', ['z', 'z']], 'x'), ('mux4 known select', ['mux', '10', ['0', '1', '1', '0']], '1'), ('decoder unknown select bit', ['dec', '1x', ['1']], ['0', '0', 'x', 'x']), ('decoder unknown enable', ['dec', '01', ['x']], ['0', 'x', '0', '0']), ('decoder enabled', ['dec', '10', ['1']], ['0', '0', '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 fixture	Actual	Expected	Outcome
mux unknown select differing data	`x`	`x`	Passed
mux unknown select agreeing data	`1`	`1`	Passed
mux4 unknown low select bit	`1`	`1`	Passed
mux4 unknown high select bit	`1`	`1`	Passed
mux unknown select floating data	`x`	`x`	Passed
mux4 known select	`1`	`1`	Passed
decoder unknown select bit	`['0', '0', 'x', 'x']`	`['0', '0', 'x', 'x']`	Passed
decoder unknown enable	`['0', 'x', '0', '0']`	`['0', 'x', '0', '0']`	Passed
decoder enabled	`['0', '0', '1', '0']`	`['0', '0', '1', '0']`	Passed

SHA-256 / 8673d97b56497630377f3c12cca4a2bc8e03f57290cb8ffe5e12bf0f7ed0ed3b

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

Case digest / be3256ee713fd175f38bd02a738e86b182f6f5fd307bd627a3f24fcc086d3acd