nx_fpga_lut_gate.nx source

1import "nx_gate_gn.nx" 2import "nx_gate_base.nx" 3// nx_fpga_lut_gate.nx -- GATE for RUNG 4 of the sovereign FPGA-boot sim: the LUT4/DFF fabric primitives + the 4// gate->LUT4 tech-map (nx_fpga_lut). EXHAUSTIVELY proven (a LUT4 has only 16 input combos, so every claim is 5// checked over its WHOLE truth table -- no sampling). Never-brick by construction is asserted mechanically. 6// T1 LUT-IS-BITSTREAM -- a LUT4 configured by init bits outputs exactly that truth table (all 16 combos). 7// T2 TECH-MAP EXACT -- every single-LUT-mappable primitive (AND/OR/NOT/XOR/NAND/NOR/XNOR/MUX) compiles to 8// a LUT4 init whose evaluation == the INDEPENDENT golden gate_ref, over ALL 16 combos. 9// T3 DFF SEQUENTIAL -- Q holds without a tick, latches D on a tick (the fabric's sequential atom). 10// T4 NEVER-BRICK -- every LUT output is in {0,1} (bounded/total) AND deterministic (same in -> same out); 11// a simulator writes NO real hardware state. (#26 by construction.) 12// T5 LIAR-KILL -- the AND-LUT does NOT reproduce XOR (a real mismatch exists) -> the check distinguishes 13// functions, not a rubber stamp; and a wide-arithmetic kind (ADD) reports NOT-single-LUT-mappable. 14// GREEN iff all pass. expect_exit: 0 license_tier: ORIGINAL 15import "nx_fpga_lut.nx" 16import "nx_syscalls.nx" 17 18func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw(" PASS " as *u8) } else { gw(" FAIL " as *u8) } gw(name); gw(" 19" as *u8); return ok } 20 21func main() -> i64 { 22 gw("=== nx_fpga_lut_gate: RUNG 4 FPGA fabric primitives (LUT4/DFF) + gate->LUT4 tech-map, exhaustively proven ===\n" as *u8) 23 var pass: i64 = 0; var total: i64 = 0 24 25 // ---- T1: a LUT4 IS its bitstream -- output bit i for input-index i, all 16 combos ---- 26 // Use XOR's truth table as a concrete init and confirm lut4_eval returns exactly that bit. 27 let xinit: i64 = fl_gate_to_lut4(FL_XOR) 28 var t1ok: i64 = 1 29 var i: i64 = 0 30 while i < 16 { 31 let a: i64 = i & 1; let b: i64 = (i>>1)&1; let c: i64 = (i>>2)&1; let d: i64 = (i>>3)&1 32 let want: i64 = (xinit >> lut4_index(a,b,c,d)) & 1 33 if lut4_eval(xinit, a, b, c, d) != want { t1ok = 0 } 34 i = i + 1 35 } 36 total=total+1; if t1ok==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 37 gw("T1 LUT4 is its bitstream: configured cell outputs exactly its 16-bit truth table (init=" as *u8); gn(xinit); gw(")\n" as *u8) 38 39 // ---- T2: TECH-MAP EXACT over every single-LUT-mappable primitive, ALL 16 combos each ---- 40 let kinds: *i64 = sys_mmap(8 * 16) as *i64 41 kinds[0]=FL_AND; kinds[1]=FL_OR; kinds[2]=FL_NOT; kinds[3]=FL_XOR; kinds[4]=FL_NAND; kinds[5]=FL_NOR; kinds[6]=FL_XNOR; kinds[7]=FL_MUX 42 let nk: i64 = 8 43 var checks: i64 = 0; var mism: i64 = 0 44 var ki: i64 = 0 45 while ki < nk { 46 let kind: i64 = kinds[ki] 47 let init: i64 = fl_gate_to_lut4(kind) 48 var j: i64 = 0 49 while j < 16 { 50 let a: i64 = j & 1; let b: i64 = (j>>1)&1; let c: i64 = (j>>2)&1; let d: i64 = (j>>3)&1 51 checks = checks + 1 52 if lut4_eval(init, a, b, c, d) != fl_gate_ref(kind, a, b, c, d) { mism = mism + 1 } 53 j = j + 1 54 } 55 ki = ki + 1 56 } 57 total=total+1; if mism==0 { if checks==128 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } } else { gw(" [FAIL] " as *u8) } 58 gw("T2 tech-map exact: " as *u8); gn(nk); gw(" primitives x 16 combos = " as *u8); gn(checks); gw(" checks, mismatches=" as *u8); gn(mism); gw(" (each primitive -> ONE LUT4)\n" as *u8) 59 60 // ---- T3: DFF sequential -- holds without a tick, latches D on a tick ---- 61 var t3ok: i64 = 1 62 if fl_dff_next(0, 1, 0) != 0 { t3ok = 0 } // no tick: keep Q=0 even though D=1 63 if fl_dff_next(1, 0, 0) != 1 { t3ok = 0 } // no tick: keep Q=1 64 if fl_dff_next(0, 1, 1) != 1 { t3ok = 0 } // tick: latch D=1 65 if fl_dff_next(1, 0, 1) != 0 { t3ok = 0 } // tick: latch D=0 66 total=total+1; if t3ok==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 67 gw("T3 DFF sequential: Q holds without clock, latches D on tick\n" as *u8) 68 69 // ---- T4: NEVER-BRICK -- bounded/total (every output in {0,1}) + deterministic ---- 70 var t4ok: i64 = 1 71 var kk: i64 = 0 72 while kk < nk { 73 let init: i64 = fl_gate_to_lut4(kinds[kk]) 74 var m: i64 = 0 75 while m < 16 { 76 let a: i64 = m & 1; let b: i64 = (m>>1)&1; let c: i64 = (m>>2)&1; let d: i64 = (m>>3)&1 77 let o1: i64 = lut4_eval(init, a, b, c, d) 78 let o2: i64 = lut4_eval(init, a, b, c, d) 79 if o1 != o2 { t4ok = 0 } // deterministic 80 if o1 < 0 { t4ok = 0 } // bounded 81 if o1 > 1 { t4ok = 0 } 82 m = m + 1 83 } 84 kk = kk + 1 85 } 86 total=total+1; if t4ok==1 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } 87 gw("T4 never-brick (#26): every LUT output in {0,1}, deterministic, zero hardware-state writes (pure in-memory sim)\n" as *u8) 88 89 // ---- T5: LIAR-KILL -- the AND-LUT must NOT reproduce XOR (a real mismatch exists) + ADD is NOT single-LUT-mappable ---- 90 let and_init: i64 = fl_gate_to_lut4(FL_AND) 91 var differs: i64 = 0 92 var z: i64 = 0 93 while z < 16 { 94 let a: i64 = z & 1; let b: i64 = (z>>1)&1; let c: i64 = (z>>2)&1; let d: i64 = (z>>3)&1 95 if lut4_eval(and_init, a, b, c, d) != fl_gate_ref(FL_XOR, a, b, c, d) { differs = differs + 1 } 96 z = z + 1 97 } 98 let add_unmappable: i64 = fl_kind_lutmappable(7) // ADD = wide arithmetic -> NOT one LUT4 99 total=total+1; if differs > 0 { if add_unmappable == 0 { pass=pass+1; gw(" [PASS] " as *u8) } else { gw(" [FAIL] " as *u8) } } else { gw(" [FAIL] " as *u8) } 100 gw("T5 liar-kill: AND-LUT != XOR in " as *u8); gn(differs); gw("/16 combos (test distinguishes functions); ADD not-single-LUT-mappable=" as *u8); if add_unmappable==0 { gw("YES\n" as *u8) } else { gw("NO\n" as *u8) } 101 102 gw("\n=== nx_fpga_lut_gate " as *u8); gn(pass); gw("/" as *u8); gn(total) 103 if pass == total { gw(" GREEN (FPGA fabric primitives modeled from spec; every gate primitive tech-maps into a bitstream-configured LUT4, exhaustively; never-brick by construction)\n" as *u8); sys_exit(0); return 0 } 104 gw(" RED\n" as *u8); sys_exit(1); return 1 105}