nx_alu_divider_floor_test.nx source

1// nx_alu_divider_floor_test.nx -- COMPLETE THE FLOOR (honest step 0 toward the 2// real divider exceed). The original floor was incomplete: it used a SIGNED 3// compare for an unsigned remainder, so it broke for large operands (the rem<<1 4// overflow into the sign bit). Now the divider uses LTU (true unsigned compare), 5// so it is correct over the FULL non-negative i64 range, INCLUDING the large-b 6// overflow cases the signed compare got wrong. 7// 8// Verified here at width 63 over the whole non-negative range: 200000 randomized 9// (a,b) in [0, 2^63) via an LCG -- which naturally exercises b in (2^62, 2^63) 10// where rem<<1 overflows the sign bit and LTU is REQUIRED -- plus a few edges, 11// each checked 1:1 vs behavioral a/b + a%b (signed `/` is a valid oracle since 12// both operands are < 2^63). HONEST: this is heavy RANDOMIZED testing over the 13// full range (exhaustive is impossible at 63-bit) -- a completed FLOOR, NOT yet 14// the machine-checked-proof EXCEED (that needs a sovereign BMC/equivalence 15// engine; full 64-bit unsigned with b>=2^63 needs >64-bit intermediates; signed 16// division also still owed). 17// 18// Known answer (FAIL LOUD): "200003 200003 " (ok, total). exit 0 iff ok==total. 19 20import "nx_alu_divider.nx" 21 22const MASK63: i64 = 9223372036854775807 // 2^63 - 1 23const LCG_A: i64 = 6364136223846793005 24const LCG_C: i64 = 1442695040888963407 25 26func _emit_num(v: i64) -> i64 { 27 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n } 28 let t2: *u8 = sys_mmap(28); var t: i64 = 0 29 if n == 0 { t2[0] = 48; t = 1 } 30 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 } 31 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 } 32 b[t] = 32; sys_write(1, b, t + 1); return 0 33} 34func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } 35 36func main() -> i64 { 37 let vals: *i64 = sys_mmap(1024 * 8) as *i64 38 let cells: *NxGsimCell = sys_mmap(1024 * 48) as *NxGsimCell 39 let g: *NxGsim = sys_mmap(64) as *NxGsim 40 g.vals = vals; g.n_nets = 2; g.cells = cells; g.n_cells = 0 41 let ro: *i64 = sys_mmap(8) as *i64; ro[0] = 0 42 let quo: i64 = nx_div_synth(g, 0, 1, 63, ro) // width-63 divider 43 let rem: i64 = ro[0] 44 45 var total: i64 = 0 46 var ok: i64 = 0 47 48 // explicit edges (incl. the large-b overflow region where LTU is required) 49 let ea: *i64 = sys_mmap(8 * 3) as *i64 50 let eb: *i64 = sys_mmap(8 * 3) as *i64 51 ea[0] = MASK63; eb[0] = 4611686018427387905 // a=2^63-1, b=2^62+1 (rem<<1 overflows sign bit) 52 ea[1] = MASK63; eb[1] = 1 // b=1 53 ea[2] = 12345; eb[2] = 9223372036854775806 // a < b, b near 2^63 54 var e: i64 = 0 55 while e < 3 { 56 g.vals[0] = ea[e]; g.vals[1] = eb[e] 57 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(20); return 20 } 58 let q: i64 = g.vals[quo]; let r: i64 = g.vals[rem] 59 let bq: i64 = ea[e] / eb[e] 60 total = total + 1 61 if q == bq { if r == ea[e] - bq * eb[e] { ok = ok + 1 } } 62 e = e + 1 63 } 64 65 // 200000 randomized (a,b) in [0, 2^63) 66 var seed: i64 = 88172645463325252 67 var nrand: i64 = 0 68 while nrand < 200000 { 69 seed = seed * LCG_A + LCG_C 70 let a: i64 = seed & MASK63 71 seed = seed * LCG_A + LCG_C 72 var b: i64 = seed & MASK63 73 if b == 0 { b = 1 } 74 g.vals[0] = a; g.vals[1] = b 75 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(21); return 21 } 76 let q: i64 = g.vals[quo]; let r: i64 = g.vals[rem] 77 let bq: i64 = a / b 78 total = total + 1 79 if q == bq { if r == a - bq * b { ok = ok + 1 } } 80 nrand = nrand + 1 81 } 82 83 _emit_num(ok); _emit_num(total); _nl() 84 if ok != total { sys_exit(1); return 1 } // every case correct (full non-neg range) 85 if total != 200003 { sys_exit(2); return 2 } 86 sys_exit(0); return 0 87}