FA-88841 / Digital logic simulation / Open access

Unknown input overrides a controlling zero on an AND gate · case 01

An AND gate with a 0 input and an unknown input reports x instead of the definite 0.

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

ROOT CAUSE

The AND evaluation tests for unknown inputs before testing for the controlling value 0.

VERIFIED REPAIR

Check for any 0 input first; only fall back to x when no controlling value is present and not all inputs are 1.

Unsuccessful approach: Checking only the first input for the controlling zero misses a 0 that arrives on a later pin.

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 == '0' else ('x' if e == 'x' else d)
    if gate in ('and', 'nand'):
        r = 'x' if 'x' in ins else ('0' if '0' in ins else '1')
    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	`x`	`0`	Failed
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 / 61a4b714f0db984300e04b07e1ae052d3620ea47e200566a40df5305ef5f4463

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' else d)
    if gate in ('and', 'nand'):
        r = '0' if ins[0] == '0' 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	`x`	`0`	Failed
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 / f87abf4b2936f443f87a7d28201b638422691a887483a2803a7ec3227b398725

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

Case digest / 3b8bb344b2910a532033d2d2532d95a1dfe9a31b320d07d86ca3ff99dfe570c1