nx_alu_divider_exhaustive_test.nx source

1// nx_alu_divider_exhaustive_test.nx -- the divider EXCEED on the VERIFICATION 2// dimension: prove the synthesized divider correct over the ENTIRE 8-bit input 3// space (all dividends 0..255 x all divisors 1..255 = 65280 pairs), quotient AND 4// remainder, 1:1 vs behavioral. 5// 6// MEET (floor) = a correct divider on a few vectors. EXCEED (this) = correctness 7// PROVEN-BY-CONSTRUCTION at 100% input-space coverage -- the guarantee incumbent 8// synthesis flows (Yosys/ABC) do NOT give (structural-only; can silently 9// miscompile -- the SynFuzz finding). Named incumbent: an unverified emitted 10// divider. Measurable dimension: verified-coverage = 100% (65280/65280). 11// 12// (This is the VERIFICATION exceed; the PERFORMANCE exceed = radix-4 SRT fewer 13// stages, scoped next by the exceed-calibration. Honest: don't conflate them.) 14// 15// Known answer (FAIL LOUD): "65280 65280 " (ok, total). exit 0 iff ok == total. 16 17import "nx_alu_divider.nx" 18 19func _emit_num(v: i64) -> i64 { 20 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n } 21 let t2: *u8 = sys_mmap(28); var t: i64 = 0 22 if n == 0 { t2[0] = 48; t = 1 } 23 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 } 24 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 } 25 b[t] = 32; sys_write(1, b, t + 1); return 0 26} 27func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } 28 29func main() -> i64 { 30 let vals: *i64 = sys_mmap(512 * 8) as *i64 31 let cells: *NxGsimCell = sys_mmap(512 * 48) as *NxGsimCell 32 let g: *NxGsim = sys_mmap(64) as *NxGsim 33 g.vals = vals 34 g.n_nets = 2 35 g.cells = cells 36 g.n_cells = 0 37 38 let rem_out: *i64 = sys_mmap(8) as *i64 39 rem_out[0] = 0 40 let quo_net: i64 = nx_div_synth(g, 0, 1, 8, rem_out) 41 let rem_net: i64 = rem_out[0] 42 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 g.vals[0] = a 50 g.vals[1] = b 51 if nx_gsim_run(g) != NX_GSIM_OK { sys_exit(20); return 20 } 52 let q: i64 = g.vals[quo_net] 53 let r: i64 = g.vals[rem_net] 54 let bq: i64 = a / b 55 let br: i64 = a - bq * b 56 total = total + 1 57 if q == bq { if r == br { ok = ok + 1 } } 58 b = b + 1 59 } 60 a = a + 1 61 } 62 63 _emit_num(ok); _emit_num(total); _nl() 64 if ok != total { sys_exit(1); return 1 } // every input pair must verify 65 if total != 65280 { sys_exit(2); return 2 } // 256 dividends x 255 divisors 66 sys_exit(0); return 0 67}