nx_alu_divider_r4_test.nx source

1// nx_alu_divider_r4_test.nx -- the divider's FULL qual+quant exceed proof. 2// QUAL: radix-4 divider exhaustively correct over the whole 8-bit space. 3// QUANT: radix-4 has FEWER subtract-stages than radix-2 (measured from the 4// netlist by counting SUB cells = the sequential remainder-update depth). 5// A full S-class exceed = BOTH (faster AND still 100%-correct). Honest scope: 6// this is the STAGE-COUNT (iteration-latency) quant win; the further SRT 7// carry-save (no carry-propagate add in the loop) win is a later step. 8// 9// Known answer (FAIL LOUD): "65280 65280 4 8 " = ok, total, r4_subtract_stages, 10// r2_subtract_stages. exit 0 iff 100%-correct AND r4_subs < r2_subs. 11 12import "nx_alu_divider_r4.nx" 13 14func _emit_num(v: i64) -> i64 { 15 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n } 16 let t2: *u8 = sys_mmap(28); var t: i64 = 0 17 if n == 0 { t2[0] = 48; t = 1 } 18 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 } 19 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 } 20 b[t] = 32; sys_write(1, b, t + 1); return 0 21} 22func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } 23 24func count_kind(g: *NxGsim, kind: i64) -> i64 { 25 var c: i64 = 0 26 var i: i64 = 0 27 while i < g.n_cells { if g.cells[i].kind == kind { c = c + 1 } i = i + 1 } 28 return c 29} 30 31func main() -> i64 { 32 // ---- radix-4 divider ---- 33 let v4: *i64 = sys_mmap(512 * 8) as *i64 34 let c4: *NxGsimCell = sys_mmap(512 * 48) as *NxGsimCell 35 let g4: *NxGsim = sys_mmap(64) as *NxGsim 36 g4.vals = v4; g4.n_nets = 2; g4.cells = c4; g4.n_cells = 0 37 let ro4: *i64 = sys_mmap(8) as *i64; ro4[0] = 0 38 let quo4: i64 = nx_div_synth_r4(g4, 0, 1, 8, ro4) 39 let rem4: i64 = ro4[0] 40 let subs4: i64 = count_kind(g4, NX_GATE_KIND_SUB) 41 42 // QUAL: exhaustive verification over the whole 8-bit space 43 var total: i64 = 0 44 var ok: i64 = 0 45 var a: i64 = 0 46 while a < 256 { 47 var b: i64 = 1 48 while b < 256 { 49 g4.vals[0] = a; g4.vals[1] = b 50 if nx_gsim_run(g4) != NX_GSIM_OK { sys_exit(20); return 20 } 51 let q: i64 = g4.vals[quo4]; let r: i64 = g4.vals[rem4] 52 let bq: i64 = a / b 53 total = total + 1 54 if q == bq { if r == a - bq * b { ok = ok + 1 } } 55 b = b + 1 56 } 57 a = a + 1 58 } 59 60 // ---- radix-2 baseline (for the QUANT stage comparison) ---- 61 let v2: *i64 = sys_mmap(512 * 8) as *i64 62 let c2: *NxGsimCell = sys_mmap(512 * 48) as *NxGsimCell 63 let g2: *NxGsim = sys_mmap(64) as *NxGsim 64 g2.vals = v2; g2.n_nets = 2; g2.cells = c2; g2.n_cells = 0 65 let ro2: *i64 = sys_mmap(8) as *i64; ro2[0] = 0 66 let dummy: i64 = nx_div_synth(g2, 0, 1, 8, ro2) 67 let subs2: i64 = count_kind(g2, NX_GATE_KIND_SUB) 68 69 _emit_num(ok); _emit_num(total); _emit_num(subs4); _emit_num(subs2); _nl() 70 71 if ok != total { sys_exit(1); return 1 } // QUAL: radix-4 100%-correct 72 if total != 65280 { sys_exit(2); return 2 } 73 if subs4 >= subs2 { sys_exit(3); return 3 } // QUANT: radix-4 fewer subtract-stages 74 sys_exit(0); return 0 75}