nx_alu_divider_alu_test.nx source

1// nx_alu_divider_alu_test.nx -- HARDWARE INVENTIONS verified IN the ALU. Builds 2// the ALU op-select netlist with the proven restoring divider (nx_div_synth) 3// wired into DIV/DIVU/REM/REMU AND the proven wide multiplier (nx_mul_wide) wired 4// into MULH/MULHSU/MULHU (high-product + sign corrections), then censuses every 5// op vs the behavioral oracle nx_rv64im_alu_compute. Compared to the stub census 6// (gate_nx_alu_netlist_full = match 17 / diverge 11), seven ops FLIP to MATCH: 7// the Verifier PROVES the divider + the mulh high-product replaced the stubs, 8// gate-level, inside the full ALU. 9// 10// a=20 b=4. Known answer (FAIL LOUD): "covered=28 match=28 diverge=0" rc=0 -- 11// the FULL RV64IM ALU verified gate-level, ZERO holes. All 28 ops match behavioral: 12// the divider (DIV/DIVU/REM/REMU), the wide-mul high-product (MULH/MULHSU/MULHU), 13// and the 32-bit W-variants (DIVUW/REMUW/DIVW/REMW, mask->32-bit divide->sext32, 14// signed via abs+sign-correct). Hardened: divider 5 vectors, mulh 5 (neg/max), 15// W-unsigned 5 (large/sext/div0), W-signed 6 (all sign combos + INT_MIN/-1 + div0). 16 17import "nx_alu_netlist_build_div.nx" 18import "rv64im_min_alu.nx" 19 20func _emit_cstr(s: *u8) -> i64 { 21 var n: i64 = 0 22 while s[n] != (0 as u8) { n = n + 1 } 23 sys_write(1, s, n) 24 return 0 25} 26 27func _emit_dec(v: i64) -> i64 { 28 let b: *u8 = sys_mmap(28) 29 let t2: *u8 = sys_mmap(28) 30 var n: i64 = v 31 if n < 0 { n = 0 - n } 32 var t: i64 = 0 33 if n == 0 { t2[0] = 48; t = 1 } 34 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 } 35 var i: i64 = 0 36 while i < t { b[i] = t2[t - 1 - i]; i = i + 1 } 37 sys_write(1, b, t) 38 return 0 39} 40 41// Re-evaluate the netlist for (a,b) at op, return 1 iff gate == behavioral. 42func _div_check(g: *NxGsim, info: *NxAluNetlist, a: i64, b: i64, op: i64) -> i64 { 43 g.vals[NX_ALUNL_A] = a 44 g.vals[NX_ALUNL_B] = b 45 g.vals[NX_ALUNL_OPIN] = op 46 if nx_gsim_run(g) != NX_GSIM_OK { return 0 - 1 } 47 let got: i64 = g.vals[info.result] 48 let beh: i64 = nx_rv64im_alu_compute(op, a, b) 49 if got == beh { return 1 } 50 return 0 51} 52 53func main() -> i64 { 54 let cells: *NxGsimCell = sys_mmap(48 * 8000) as *NxGsimCell 55 let vals: *i64 = sys_mmap(8 * 8000) as *i64 56 let info: *NxAluNetlist = sys_mmap(64) as *NxAluNetlist 57 let g: *NxGsim = sys_mmap(64) as *NxGsim 58 59 g.vals = vals 60 g.cells = cells 61 nx_alu_netlist_build_div(g, info) 62 g.n_nets = info.n_nets 63 g.n_cells = info.n_cells 64 65 let a: i64 = 20 66 let b: i64 = 4 67 68 var n_match: i64 = 0 69 var n_div: i64 = 0 70 var div_ok: i64 = 0 71 var divu_ok: i64 = 0 72 var rem_ok: i64 = 0 73 var remu_ok: i64 = 0 74 var mhu_ok: i64 = 0 75 var mh_ok: i64 = 0 76 var mhsu_ok: i64 = 0 77 var divuw_ok: i64 = 0 78 var remuw_ok: i64 = 0 79 var divw_ok: i64 = 0 80 var remw_ok: i64 = 0 81 82 var op: i64 = 1 83 while op < NX_RV64IM_ALU_N { 84 vals[NX_ALUNL_A] = a 85 vals[NX_ALUNL_B] = b 86 vals[NX_ALUNL_OPIN] = op 87 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(40); return 40 } 88 let got: i64 = vals[info.result] 89 let beh: i64 = nx_rv64im_alu_compute(op, a, b) 90 if got == beh { n_match = n_match + 1 } 91 if got != beh { n_div = n_div + 1 } 92 if op == NX_RV64IM_ALU_DIV { if got == beh { div_ok = 1 } } 93 if op == NX_RV64IM_ALU_DIVU { if got == beh { divu_ok = 1 } } 94 if op == NX_RV64IM_ALU_REM { if got == beh { rem_ok = 1 } } 95 if op == NX_RV64IM_ALU_REMU { if got == beh { remu_ok = 1 } } 96 if op == NX_RV64IM_ALU_MULHU { if got == beh { mhu_ok = 1 } } 97 if op == NX_RV64IM_ALU_MULH { if got == beh { mh_ok = 1 } } 98 if op == NX_RV64IM_ALU_MULHSU { if got == beh { mhsu_ok = 1 } } 99 if op == NX_RV64IM_ALU_DIVUW { if got == beh { divuw_ok = 1 } } 100 if op == NX_RV64IM_ALU_REMUW { if got == beh { remuw_ok = 1 } } 101 if op == NX_RV64IM_ALU_DIVW { if got == beh { divw_ok = 1 } } 102 if op == NX_RV64IM_ALU_REMW { if got == beh { remw_ok = 1 } } 103 op = op + 1 104 } 105 106 _emit_cstr("covered=" as *u8) 107 _emit_dec(NX_RV64IM_ALU_N - 1) 108 _emit_cstr(" match=" as *u8) 109 _emit_dec(n_match) 110 _emit_cstr(" diverge=" as *u8) 111 _emit_dec(n_div) 112 _emit_cstr("\n" as *u8) 113 114 // Harden: the divider must match behavioral over MORE than the census vector 115 // -- q>1, r>0, a==b (q=1,r=0), a<b (q=0,r=a) -- across all 4 div/rem ops. 116 // Refutes "matches 24->5 by coincidence at (20,4)". 117 let av: *i64 = sys_mmap(8 * 5) as *i64 118 let bv: *i64 = sys_mmap(8 * 5) as *i64 119 av[0] = 100; bv[0] = 7 120 av[1] = 255; bv[1] = 16 121 av[2] = 1000; bv[2] = 3 122 av[3] = 42; bv[3] = 42 123 av[4] = 7; bv[4] = 9 124 var vi: i64 = 0 125 while vi < 5 { 126 if _div_check(g, info, av[vi], bv[vi], NX_RV64IM_ALU_DIV) != 1 { sys_exit(10); return 10 } 127 if _div_check(g, info, av[vi], bv[vi], NX_RV64IM_ALU_DIVU) != 1 { sys_exit(11); return 11 } 128 if _div_check(g, info, av[vi], bv[vi], NX_RV64IM_ALU_REM) != 1 { sys_exit(12); return 12 } 129 if _div_check(g, info, av[vi], bv[vi], NX_RV64IM_ALU_REMU) != 1 { sys_exit(13); return 13 } 130 vi = vi + 1 131 } 132 133 // Harden mulh: exercise the sign corrections (negative operands) + a nonzero 134 // high product, across MULH / MULHU / MULHSU vs behavioral. 135 let ma: *i64 = sys_mmap(8 * 5) as *i64 136 let mb: *i64 = sys_mmap(8 * 5) as *i64 137 ma[0] = 0 - 5; mb[0] = 3 // a<0 correction 138 ma[1] = 7; mb[1] = 0 - 3 // b<0 correction 139 ma[2] = 0 - 5; mb[2] = 0 - 3 // both 140 ma[3] = 1099511627776; mb[3] = 1099511627776 // 2^40 * 2^40 = 2^80 -> hi = 2^16 (nonzero) 141 ma[4] = 0 - 1; mb[4] = 0 - 1 // max-magnitude 142 var mi: i64 = 0 143 while mi < 5 { 144 if _div_check(g, info, ma[mi], mb[mi], NX_RV64IM_ALU_MULH) != 1 { sys_exit(20); return 20 } 145 if _div_check(g, info, ma[mi], mb[mi], NX_RV64IM_ALU_MULHU) != 1 { sys_exit(21); return 21 } 146 if _div_check(g, info, ma[mi], mb[mi], NX_RV64IM_ALU_MULHSU) != 1 { sys_exit(22); return 22 } 147 mi = mi + 1 148 } 149 150 if div_ok != 1 { sys_exit(1); return 1 } // DIV now matches behavioral (divider, not stub) 151 if divu_ok != 1 { sys_exit(2); return 2 } 152 if rem_ok != 1 { sys_exit(3); return 3 } 153 if remu_ok != 1 { sys_exit(4); return 4 } 154 if mhu_ok != 1 { sys_exit(5); return 5 } // mulhu now high-product via wide multiplier 155 if mh_ok != 1 { sys_exit(6); return 6 } 156 if mhsu_ok != 1 { sys_exit(7); return 7 } 157 158 // Harden the W-suffix unsigned div/rem: large 32-bit operands, a bit-31-set 159 // quotient (exercises sext32), and the div-by-zero edge. 160 let wa: *i64 = sys_mmap(8 * 5) as *i64 161 let wb: *i64 = sys_mmap(8 * 5) as *i64 162 wa[0] = 4000000000; wb[0] = 7 // large unsigned 32-bit 163 wa[1] = 4294967294; wb[1] = 1 // q=0xFFFFFFFE -> sext32 negative 164 wa[2] = 100; wb[2] = 0 // div-by-zero edge 165 wa[3] = 4294967295; wb[3] = 65535 166 wa[4] = 1000000; wb[4] = 999 // r>0 167 var wi: i64 = 0 168 while wi < 5 { 169 if _div_check(g, info, wa[wi], wb[wi], NX_RV64IM_ALU_DIVUW) != 1 { sys_exit(23); return 23 } 170 if _div_check(g, info, wa[wi], wb[wi], NX_RV64IM_ALU_REMUW) != 1 { sys_exit(24); return 24 } 171 wi = wi + 1 172 } 173 174 // Harden the W-suffix SIGNED div/rem: all four sign combinations, the 175 // INT_MIN/-1 overflow case, div-by-zero, and a remainder-sign case. 176 let sa: *i64 = sys_mmap(8 * 6) as *i64 177 let sb: *i64 = sys_mmap(8 * 6) as *i64 178 sa[0] = 0 - 7; sb[0] = 2 // -/+ 179 sa[1] = 7; sb[1] = 0 - 2 // +/- 180 sa[2] = 0 - 7; sb[2] = 0 - 2 // -/- 181 sa[3] = 0 - 2147483648; sb[3] = 0 - 1 // INT_MIN / -1 overflow 182 sa[4] = 100; sb[4] = 0 // div-by-zero 183 sa[5] = 0 - 100; sb[5] = 7 // remainder sign 184 var si: i64 = 0 185 while si < 6 { 186 if _div_check(g, info, sa[si], sb[si], NX_RV64IM_ALU_DIVW) != 1 { sys_exit(25); return 25 } 187 if _div_check(g, info, sa[si], sb[si], NX_RV64IM_ALU_REMW) != 1 { sys_exit(26); return 26 } 188 si = si + 1 189 } 190 191 if divuw_ok != 1 { sys_exit(8); return 8 } 192 if remuw_ok != 1 { sys_exit(9); return 9 } 193 if divw_ok != 1 { sys_exit(10); return 10 } 194 if remw_ok != 1 { sys_exit(11); return 11 } 195 if n_match != 28 { sys_exit(12); return 12 } 196 if n_div != 0 { sys_exit(13); return 13 } 197 sys_exit(0) 198 return 0 199}