nx_nxgate_sim_test.nx source

1// nx_nxgate_sim_test.nx -- proof-of-life GATE for the gate-level functional 2// simulator (VERIFIER organ's hardware oracle, SIL-3). 3// 4// Builds a small word-level netlist by hand and proves: 5// (1) the simulator EVALUATES combinational cells correctly (XOR/ADD/SUB/MUL/ 6// EQ/MUX) over an input vector; 7// (2) it CATCHES the SIL-1 stub class: a DIV represented as an ADD cell (what 8// the ALU gate emitter actually emits today) DIVERGES from behavioral DIV 9// -- the divergence the verifier exists to surface. 10// 11// Vector a=12 b=4. Known answer (FAIL LOUD): "8 16 8 48 0 16 16 3 " = 12// xor add sub mul eq mux divstub realdiv. (divstub=16 != realdiv=3 -> caught) 13 14import "nx_nxgate_sim.nx" 15 16func _emit_num(v: i64) -> i64 { 17 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n } 18 let t2: *u8 = sys_mmap(28); var t: i64 = 0 19 if n == 0 { t2[0] = 48; t = 1 } 20 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 } 21 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 } 22 b[t] = 32; sys_write(1, b, t + 1); return 0 23} 24func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } 25 26func main() -> i64 { 27 let vals: *i64 = sys_mmap(64 * 8) as *i64 28 let cells: *NxGsimCell = sys_mmap(16 * 40) as *NxGsimCell 29 let g: *NxGsim = sys_mmap(64) as *NxGsim 30 g.vals = vals 31 g.n_nets = 9 32 g.cells = cells 33 g.n_cells = 7 34 35 // nets: 0=a 1=b (inputs); 2=xor 3=add 4=sub 5=mul 6=eq 7=mux 8=divstub 36 cells[0].kind = NX_GATE_KIND_XOR; cells[0].fanout = 2; cells[0].f0 = 0; cells[0].f1 = 1; cells[0].f2 = 0 - 1 37 cells[1].kind = NX_GATE_KIND_ADD; cells[1].fanout = 3; cells[1].f0 = 0; cells[1].f1 = 1; cells[1].f2 = 0 - 1 38 cells[2].kind = NX_GATE_KIND_SUB; cells[2].fanout = 4; cells[2].f0 = 0; cells[2].f1 = 1; cells[2].f2 = 0 - 1 39 cells[3].kind = NX_GATE_KIND_MUL; cells[3].fanout = 5; cells[3].f0 = 0; cells[3].f1 = 1; cells[3].f2 = 0 - 1 40 cells[4].kind = NX_GATE_KIND_EQ; cells[4].fanout = 6; cells[4].f0 = 0; cells[4].f1 = 1; cells[4].f2 = 0 - 1 41 // mux (emitter convention sel?this:prev): sel=net6(eq=0), this=net4(sub=8), prev=net3(add=16) -> sel==0 picks prev=16 42 cells[5].kind = NX_GATE_KIND_MUX; cells[5].fanout = 7; cells[5].f0 = 6; cells[5].f1 = 4; cells[5].f2 = 3 43 // the SIL-1 stub: ALU emits an ADD cell where DIV belongs 44 cells[6].kind = NX_GATE_KIND_ADD; cells[6].fanout = 8; cells[6].f0 = 0; cells[6].f1 = 1; cells[6].f2 = 0 - 1 45 46 vals[0] = 12 47 vals[1] = 4 48 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(10); return 10 } 49 50 let xr: i64 = vals[2] 51 let ar: i64 = vals[3] 52 let sr: i64 = vals[4] 53 let mr: i64 = vals[5] 54 let er: i64 = vals[6] 55 let xm: i64 = vals[7] 56 let dv: i64 = vals[8] 57 let real_div: i64 = 12 / 4 58 _emit_num(xr); _emit_num(ar); _emit_num(sr); _emit_num(mr); _emit_num(er); _emit_num(xm); _emit_num(dv); _emit_num(real_div) 59 _nl() 60 61 if xr != 8 { sys_exit(1); return 1 } // 12 ^ 4 62 if ar != 16 { sys_exit(2); return 2 } // 12 + 4 63 if sr != 8 { sys_exit(3); return 3 } // 12 - 4 64 if mr != 48 { sys_exit(4); return 4 } // 12 * 4 65 if er != 0 { sys_exit(5); return 5 } // 12 == 4 -> 0 66 if xm != 16 { sys_exit(6); return 6 } // MUX sel=0 -> in0 (add=16) 67 if dv == real_div { sys_exit(7); return 7 } // STUB CATCH: ADD(16) must NOT equal DIV(3) 68 sys_exit(0); return 0 69}