{"abstract":"A decoder with one unknown select bit drives x on lines that cannot be selected.","category":"Digital logic simulation","checks":9,"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'.","contract_signature":"*args","evaluation_group":"w2-digital-logic-simulation-xsel-mux-decoder","failed_approach":"An unknown enable still spreads x onto non-candidate lines.","family":"w2-digital-logic-simulation-xsel-mux-decoder-decoder-candidate-lines","id":"FA-89236","implementations":{"attempt":{"sha256":"e212ae6f8599edbe9e6dd56863f4f3843e38a5bb93e68c03c3e1a9dae6b862d5","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(*args):\n    kind, sel, data = args\n    cands = [0]\n    for s in sel:\n        if s in '01':\n            cands = [c * 2 + int(s) for c in cands]\n        else:\n            cands = [c * 2 + b for c in cands for b in (0, 1)]\n    if kind == 'mux':\n        vals = sorted({data[c] for c in cands})\n        return vals[0] if len(vals) == 1 and vals[0] in '01' else 'x'\n    en = data[0]\n    out = []\n    for i in range(2 ** len(sel)):\n        if en == '0':\n            out.append('0')\n        elif len(cands) > 1 and i in cands or en == 'x':\n            out.append('x')\n        elif i in cands:\n            out.append('1')\n        else:\n            out.append('0')\n    return out\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nfixtures = [[('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'])]]\nfor label, args, expected in fixtures[N-1]:\n    check(label, solve(*args), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"broken":{"sha256":"228370b1c80770ff94c8fba344f8c658dd030f86413fa16bdb489ca7cdcf2077","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(*args):\n    kind, sel, data = args\n    cands = [0]\n    for s in sel:\n        if s in '01':\n            cands = [c * 2 + int(s) for c in cands]\n        else:\n            cands = [c * 2 + b for c in cands for b in (0, 1)]\n    if kind == 'mux':\n        vals = sorted({data[c] for c in cands})\n        return vals[0] if len(vals) == 1 and vals[0] in '01' else 'x'\n    en = data[0]\n    out = []\n    for i in range(2 ** len(sel)):\n        if en == '0':\n            out.append('0')\n        elif len(cands) > 1 or en != '1':\n            out.append('x')\n        elif i in cands:\n            out.append('1')\n        else:\n            out.append('0')\n    return out\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nfixtures = [[('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'])]]\nfor label, args, expected in fixtures[N-1]:\n    check(label, solve(*args), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"}},"limitations":"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.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"w2-digital-logic-simulation-xsel-mux-decoder-decoder-candidate-lines","generated_at":"2026-09-29T14:51:15.551955+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"Unknown-select pessimism rules in RTL simulation decide whether X on a control input corrupts datapath outputs.","root_cause":"The unknown case does not restrict itself to candidate lines.","sha256":"eb9bea72a3e1766142e9d6df5ab8e3c5c8c88c4e7e409b1356f1bb52d750743b","title":"Unknown select corrupts every decoder line · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verified":true,"visibility":"public","verification":{"attempt":{"elapsed_ms":39.122,"exit_code":1,"observations":[{"actual":"x","check":"mux unknown select differing data","expected":"x","passed":true},{"actual":"1","check":"mux unknown select agreeing data","expected":"1","passed":true},{"actual":"1","check":"mux4 unknown low select bit","expected":"1","passed":true},{"actual":"1","check":"mux4 unknown high select bit","expected":"1","passed":true},{"actual":"x","check":"mux unknown select floating data","expected":"x","passed":true},{"actual":"1","check":"mux4 known select","expected":"1","passed":true},{"actual":["0","0","x","x"],"check":"decoder unknown select bit","expected":["0","0","x","x"],"passed":true},{"actual":["x","x","x","x"],"check":"decoder unknown enable","expected":["0","x","0","0"],"passed":false},{"actual":["0","0","1","0"],"check":"decoder enabled","expected":["0","0","1","0"],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"mux unknown select differing data\", \"actual\": \"x\", \"expected\": \"x\", \"passed\": true}, {\"check\": \"mux unknown select agreeing data\", \"actual\": \"1\", \"expected\": \"1\", \"passed\": true}, {\"check\": \"mux4 unknown low select bit\", \"actual\": \"1\", \"expected\": \"1\", \"passed\": true}, {\"check\": \"mux4 unknown high select bit\", \"actual\": \"1\", \"expected\": \"1\", \"passed\": true}, {\"check\": \"mux unknown select floating data\", \"actual\": \"x\", \"expected\": \"x\", \"passed\": true}, {\"check\": \"mux4 known select\", \"actual\": \"1\", \"expected\": \"1\", \"passed\": true}, {\"check\": \"decoder unknown select bit\", \"actual\": [\"0\", \"0\", \"x\", \"x\"], \"expected\": [\"0\", \"0\", \"x\", \"x\"], \"passed\": true}, {\"check\": \"decoder unknown enable\", \"actual\": [\"x\", \"x\", \"x\", \"x\"], \"expected\": [\"0\", \"x\", \"0\", \"0\"], \"passed\": false}, {\"check\": \"decoder enabled\", \"actual\": [\"0\", \"0\", \"1\", \"0\"], \"expected\": [\"0\", \"0\", \"1\", \"0\"], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":40.649,"exit_code":1,"observations":[{"actual":"x","check":"mux unknown select differing data","expected":"x","passed":true},{"actual":"1","check":"mux unknown select agreeing data","expected":"1","passed":true},{"actual":"1","check":"mux4 unknown low select bit","expected":"1","passed":true},{"actual":"1","check":"mux4 unknown high select bit","expected":"1","passed":true},{"actual":"x","check":"mux unknown select floating data","expected":"x","passed":true},{"actual":"1","check":"mux4 known select","expected":"1","passed":true},{"actual":["x","x","x","x"],"check":"decoder unknown select bit","expected":["0","0","x","x"],"passed":false},{"actual":["x","x","x","x"],"check":"decoder unknown enable","expected":["0","x","0","0"],"passed":false},{"actual":["0","0","1","0"],"check":"decoder enabled","expected":["0","0","1","0"],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"mux unknown select differing data\", \"actual\": \"x\", \"expected\": \"x\", \"passed\": true}, {\"check\": \"mux unknown select agreeing data\", \"actual\": \"1\", \"expected\": \"1\", \"passed\": true}, {\"check\": \"mux4 unknown low select bit\", \"actual\": \"1\", \"expected\": \"1\", \"passed\": true}, {\"check\": \"mux4 unknown high select bit\", \"actual\": \"1\", \"expected\": \"1\", \"passed\": true}, {\"check\": \"mux unknown select floating data\", \"actual\": \"x\", \"expected\": \"x\", \"passed\": true}, {\"check\": \"mux4 known select\", \"actual\": \"1\", \"expected\": \"1\", \"passed\": true}, {\"check\": \"decoder unknown select bit\", \"actual\": [\"x\", \"x\", \"x\", \"x\"], \"expected\": [\"0\", \"0\", \"x\", \"x\"], \"passed\": false}, {\"check\": \"decoder unknown enable\", \"actual\": [\"x\", \"x\", \"x\", \"x\"], \"expected\": [\"0\", \"x\", \"0\", \"0\"], \"passed\": false}, {\"check\": \"decoder enabled\", \"actual\": [\"0\", \"0\", \"1\", \"0\"], \"expected\": [\"0\", \"0\", \"1\", \"0\"], \"passed\": true}], \"passed\": false}\n"}},"member_only":{"stages":["fixed"],"fields":["implementations.fixed","verification.fixed","harness","repair"],"note":"The verified repair, its recorded checks, the repair description, and the scoring harness are available to members."}}