FA-88861 / Digital logic simulation / Open access

Unknown enable on a tri-state buffer releases the net · case 01

A bufif1 with an unknown enable drives 'z' instead of an unknown value.

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

ROOT CAUSE

Every enable that is not exactly 1 is treated as disabled.

VERIFIED REPAIR

Drive 'z' only for enable 0; an unknown enable must produce 'x'.

Unsuccessful approach: Passing data 0 through on an unknown enable still claims a definite level the buffer may not be driving.

Case contract

Values are '0','1','x','z'. A 'z' on any gate input is read as 'x'. and/nand: any 0 -> 0, all 1 -> 1, else x; or/nor: any 1 -> 1, all 0 -> 0, else x; xor/xnor: any x -> x, else parity of ones; buf/not use the single input; nand/nor/xnor/not invert (x stays x). bufif1(data, enable): enable 0 -> 'z', enable x/z -> 'x', enable 1 -> data (z data becomes x).

Why this case matters

Gate-level logic simulators must propagate unknown and high-impedance values without inventing definite levels.

1 / The failure

Exit 1

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

N = 1
observations = []
def solve(*args):
    gate, ins = args
    def inv(v):
        return {'0': '1', '1': '0'}.get(v, 'x')
    ins = [('x' if v == 'z' else v) for v in ins]
    if gate == 'bufif1':
        d, e = ins
        return 'z' if e != '1' else d
    if gate in ('and', 'nand'):
        r = '0' if '0' in ins else ('1' if all(v == '1' for v in ins) else 'x')
    elif gate in ('or', 'nor'):
        r = '1' if '1' in ins else ('0' if all(v == '0' for v in ins) else 'x')
    elif gate in ('xor', 'xnor'):
        r = 'x' if 'x' in ins else str(ins.count('1') % 2)
    else:
        r = ins[0]
    return inv(r) if gate in ('nand', 'nor', 'xnor', 'not') else r
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('and gate: controlling zero after unknowns', ['and', ['x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '0']], '0'), ('inverter control', ['not', ['1']], '0'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['1', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', '1']], '1')], [('and gate: controlling zero after unknowns', ['and', ['x', 'x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', '1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x', '0']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '1', '0']], '1'), ('inverter control', ['not', ['0']], '1'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['0', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', 'z', '1']], '1')], [('and gate: controlling zero after unknowns', ['and', ['x', 'x', 'x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1', '1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', '1', '1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x', '0', '0']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '1', '1', '0']], '0'), ('inverter control', ['not', ['1']], '0'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['1', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', 'z', 'z', '1']], '1')], [('and gate: controlling zero after unknowns', ['and', ['x', 'x', 'x', 'x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1', '1', '1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', '1', '1', '1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x', '0', '0', '0']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '1', '1', '1', '0']], '1'), ('inverter control', ['not', ['0']], '1'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['0', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', 'z', 'z', 'z', '1']], '1')], [('and gate: controlling zero after unknowns', ['and', ['x', 'x', 'x', 'x', 'x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1', '1', '1', '1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', '1', '1', '1', '1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x', '0', '0', '0', '0']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '1', '1', '1', '1', '0']], '0'), ('inverter control', ['not', ['1']], '0'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['1', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', 'z', 'z', 'z', 'z', '1']], '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
and gate: controlling zero after unknowns	`0`	`0`	Passed
nand gate: all ones	`0`	`0`	Passed
xor gate: floating input	`x`	`x`	Passed
buffer of a floating net	`x`	`x`	Passed
xor gate: two unknowns	`x`	`x`	Passed
xnor gate: parity inversion	`0`	`0`	Passed
inverter control	`0`	`0`	Passed
bufif1 unknown enable with low data	`z`	`x`	Failed
bufif1 unknown enable with high data	`z`	`x`	Failed
bufif1 disabled drives z	`z`	`z`	Passed
or gate: controlling one beside z	`1`	`1`	Passed

SHA-256 / 33ac38e254348fe4d505922b15f35bb622a348e18b435c3695dfdc40f7e75106

2 / The unsuccessful fix

Exit 1

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

N = 1
observations = []
def solve(*args):
    gate, ins = args
    def inv(v):
        return {'0': '1', '1': '0'}.get(v, 'x')
    ins = [('x' if v == 'z' else v) for v in ins]
    if gate == 'bufif1':
        d, e = ins
        return 'z' if e == '0' else ('x' if e == 'x' and d != '0' else d)
    if gate in ('and', 'nand'):
        r = '0' if '0' in ins else ('1' if all(v == '1' for v in ins) else 'x')
    elif gate in ('or', 'nor'):
        r = '1' if '1' in ins else ('0' if all(v == '0' for v in ins) else 'x')
    elif gate in ('xor', 'xnor'):
        r = 'x' if 'x' in ins else str(ins.count('1') % 2)
    else:
        r = ins[0]
    return inv(r) if gate in ('nand', 'nor', 'xnor', 'not') else r
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('and gate: controlling zero after unknowns', ['and', ['x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '0']], '0'), ('inverter control', ['not', ['1']], '0'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['1', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', '1']], '1')], [('and gate: controlling zero after unknowns', ['and', ['x', 'x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', '1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x', '0']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '1', '0']], '1'), ('inverter control', ['not', ['0']], '1'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['0', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', 'z', '1']], '1')], [('and gate: controlling zero after unknowns', ['and', ['x', 'x', 'x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1', '1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', '1', '1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x', '0', '0']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '1', '1', '0']], '0'), ('inverter control', ['not', ['1']], '0'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['1', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', 'z', 'z', '1']], '1')], [('and gate: controlling zero after unknowns', ['and', ['x', 'x', 'x', 'x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1', '1', '1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', '1', '1', '1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x', '0', '0', '0']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '1', '1', '1', '0']], '1'), ('inverter control', ['not', ['0']], '1'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['0', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', 'z', 'z', 'z', '1']], '1')], [('and gate: controlling zero after unknowns', ['and', ['x', 'x', 'x', 'x', 'x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1', '1', '1', '1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', '1', '1', '1', '1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x', '0', '0', '0', '0']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '1', '1', '1', '1', '0']], '0'), ('inverter control', ['not', ['1']], '0'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['1', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', 'z', 'z', 'z', 'z', '1']], '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
and gate: controlling zero after unknowns	`0`	`0`	Passed
nand gate: all ones	`0`	`0`	Passed
xor gate: floating input	`x`	`x`	Passed
buffer of a floating net	`x`	`x`	Passed
xor gate: two unknowns	`x`	`x`	Passed
xnor gate: parity inversion	`0`	`0`	Passed
inverter control	`0`	`0`	Passed
bufif1 unknown enable with low data	`0`	`x`	Failed
bufif1 unknown enable with high data	`x`	`x`	Passed
bufif1 disabled drives z	`z`	`z`	Passed
or gate: controlling one beside z	`1`	`1`	Passed

SHA-256 / 5ed32b17e443b65aaada87ae1d2770cfa3cfd23ec7ccc5470254456433dc44c8

3 / The verified repair

Exit 0

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

N = 1
observations = []
def solve(*args):
    gate, ins = args
    def inv(v):
        return {'0': '1', '1': '0'}.get(v, 'x')
    ins = [('x' if v == 'z' else v) for v in ins]
    if gate == 'bufif1':
        d, e = ins
        return 'z' if e == '0' else ('x' if e == 'x' else d)
    if gate in ('and', 'nand'):
        r = '0' if '0' in ins else ('1' if all(v == '1' for v in ins) else 'x')
    elif gate in ('or', 'nor'):
        r = '1' if '1' in ins else ('0' if all(v == '0' for v in ins) else 'x')
    elif gate in ('xor', 'xnor'):
        r = 'x' if 'x' in ins else str(ins.count('1') % 2)
    else:
        r = ins[0]
    return inv(r) if gate in ('nand', 'nor', 'xnor', 'not') else r
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('and gate: controlling zero after unknowns', ['and', ['x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '0']], '0'), ('inverter control', ['not', ['1']], '0'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['1', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', '1']], '1')], [('and gate: controlling zero after unknowns', ['and', ['x', 'x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', '1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x', '0']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '1', '0']], '1'), ('inverter control', ['not', ['0']], '1'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['0', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', 'z', '1']], '1')], [('and gate: controlling zero after unknowns', ['and', ['x', 'x', 'x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1', '1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', '1', '1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x', '0', '0']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '1', '1', '0']], '0'), ('inverter control', ['not', ['1']], '0'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['1', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', 'z', 'z', '1']], '1')], [('and gate: controlling zero after unknowns', ['and', ['x', 'x', 'x', 'x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1', '1', '1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', '1', '1', '1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x', '0', '0', '0']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '1', '1', '1', '0']], '1'), ('inverter control', ['not', ['0']], '1'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['0', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', 'z', 'z', 'z', '1']], '1')], [('and gate: controlling zero after unknowns', ['and', ['x', 'x', 'x', 'x', 'x', '0']], '0'), ('nand gate: all ones', ['nand', ['1', '1', '1', '1', '1', '1']], '0'), ('xor gate: floating input', ['xor', ['1', '1', '1', '1', '1', 'z']], 'x'), ('buffer of a floating net', ['buf', ['z']], 'x'), ('xor gate: two unknowns', ['xor', ['x', 'x', '0', '0', '0', '0']], 'x'), ('xnor gate: parity inversion', ['xnor', ['1', '1', '1', '1', '1', '0']], '0'), ('inverter control', ['not', ['1']], '0'), ('bufif1 unknown enable with low data', ['bufif1', ['0', 'x']], 'x'), ('bufif1 unknown enable with high data', ['bufif1', ['1', 'z']], 'x'), ('bufif1 disabled drives z', ['bufif1', ['1', '0']], 'z'), ('or gate: controlling one beside z', ['or', ['z', 'z', 'z', 'z', 'z', '1']], '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
and gate: controlling zero after unknowns	`0`	`0`	Passed
nand gate: all ones	`0`	`0`	Passed
xor gate: floating input	`x`	`x`	Passed
buffer of a floating net	`x`	`x`	Passed
xor gate: two unknowns	`x`	`x`	Passed
xnor gate: parity inversion	`0`	`0`	Passed
inverter control	`0`	`0`	Passed
bufif1 unknown enable with low data	`x`	`x`	Passed
bufif1 unknown enable with high data	`x`	`x`	Passed
bufif1 disabled drives z	`z`	`z`	Passed
or gate: controlling one beside z	`1`	`1`	Passed

SHA-256 / bf15fc3a903151bbaa24735361c943b11c86bac06ef93c0a5eee525770f8f941

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

Case digest / 7de6d3833744e4840e2aa0f943d4dbe7c1aca02639f3897d2d515e95c2e0a381