nx_alu_netlist_test.nx source

1// nx_alu_netlist_test.nx -- VERIFIER on the REAL ALU op-select topology 2// (SIL-3 closure, layer-7). Builds a 3-op (ADD/SUB/DIV) ALU netlist using the 3// EXACT structure the .nxgate ALU emitter (synth_emit_alu_gates.nx) emits: 4// per op a CONST(opcode) + a binop subnet + an EQ(op_in==opcode) match, then a 5// cascade MUX(match, this, prev). DIV is emitted as an ADD cell -- the SIL-1 6// stub (emitter lines 151-158, "TODO_SILICON proper divider"). 7// 8// Simulating over op_in proves: the correct ops (ADD/SUB) match the behavioral 9// ALU, and DIV (= a+b stub) DIVERGES from behavioral a/b -- the verifier CATCHES 10// the silent gate-emit miscompile via op-selection (what structural-only smokes 11// miss). 12// 13// a=20 b=4. Known answer (FAIL LOUD): "24 24 16 16 24 5 " = 14// res_add beh_add res_sub beh_sub res_div beh_div. (res_div=24 != beh=5 -> caught) 15 16import "nx_nxgate_sim.nx" 17 18func _emit_num(v: i64) -> i64 { 19 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n } 20 let t2: *u8 = sys_mmap(28); var t: i64 = 0 21 if n == 0 { t2[0] = 48; t = 1 } 22 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 } 23 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 } 24 b[t] = 32; sys_write(1, b, t + 1); return 0 25} 26func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } 27 28func _setcell(cells: *NxGsimCell, id: i64, kind: i64, fanout: i64, f0: i64, f1: i64, f2: i64) -> i64 { 29 cells[id].kind = kind 30 cells[id].fanout = fanout 31 cells[id].f0 = f0 32 cells[id].f1 = f1 33 cells[id].f2 = f2 34 return 0 35} 36 37func main() -> i64 { 38 let vals: *i64 = sys_mmap(64 * 8) as *i64 39 let cells: *NxGsimCell = sys_mmap(32 * 48) as *NxGsimCell 40 let g: *NxGsim = sys_mmap(64) as *NxGsim 41 g.vals = vals 42 g.n_nets = 16 43 g.cells = cells 44 g.n_cells = 13 45 46 // nets: 0=a 1=b 2=op_in (inputs); op codes ADD=1 SUB=2 DIV=3 47 _setcell(cells, 0, NX_GATE_KIND_CONST, 3, 0 - 1, 0 - 1, 0 - 1); cells[0].val = 1 // op-code ADD 48 _setcell(cells, 1, NX_GATE_KIND_ADD, 4, 0, 1, 0 - 1) // ADD subnet 49 _setcell(cells, 2, NX_GATE_KIND_EQ, 5, 2, 3, 0 - 1) // match ADD 50 _setcell(cells, 3, NX_GATE_KIND_CONST, 6, 0 - 1, 0 - 1, 0 - 1); cells[3].val = 2 // op-code SUB 51 _setcell(cells, 4, NX_GATE_KIND_SUB, 7, 0, 1, 0 - 1) // SUB subnet 52 _setcell(cells, 5, NX_GATE_KIND_EQ, 8, 2, 6, 0 - 1) // match SUB 53 _setcell(cells, 6, NX_GATE_KIND_CONST, 9, 0 - 1, 0 - 1, 0 - 1); cells[6].val = 3 // op-code DIV 54 _setcell(cells, 7, NX_GATE_KIND_ADD, 10, 0, 1, 0 - 1) // DIV subnet = STUB (ADD) 55 _setcell(cells, 8, NX_GATE_KIND_EQ, 11, 2, 9, 0 - 1) // match DIV 56 _setcell(cells, 9, NX_GATE_KIND_CONST,12, 0 - 1, 0 - 1, 0 - 1); cells[9].val = 0 // INVALID prev0 57 _setcell(cells, 10, NX_GATE_KIND_MUX, 13, 5, 4, 12) // matchADD ? subADD : prev 58 _setcell(cells, 11, NX_GATE_KIND_MUX, 14, 8, 7, 13) // matchSUB ? subSUB : prev 59 _setcell(cells, 12, NX_GATE_KIND_MUX, 15, 11, 10, 14) // matchDIV ? subDIV : prev 60 61 vals[0] = 20 62 vals[1] = 4 63 64 vals[2] = 1 65 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(10); return 10 } 66 let res_add: i64 = vals[15] 67 68 vals[2] = 2 69 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(11); return 11 } 70 let res_sub: i64 = vals[15] 71 72 vals[2] = 3 73 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(12); return 12 } 74 let res_div: i64 = vals[15] 75 76 let beh_add: i64 = 20 + 4 77 let beh_sub: i64 = 20 - 4 78 let beh_div: i64 = 20 / 4 79 _emit_num(res_add); _emit_num(beh_add); _emit_num(res_sub); _emit_num(beh_sub); _emit_num(res_div); _emit_num(beh_div) 80 _nl() 81 82 if res_add != beh_add { sys_exit(1); return 1 } // ADD op == behavioral ADD 83 if res_sub != beh_sub { sys_exit(2); return 2 } // SUB op == behavioral SUB 84 if res_div == beh_div { sys_exit(3); return 3 } // STUB CATCH: DIV stub(24) must NOT equal behavioral(5) 85 sys_exit(0); return 0 86}