code wiki / _hdl_build / nx_superopt_general_test.nx

nx_superopt_general_test.nx source

↩ module page · 124 lines · 5497 B

1// nx_superopt_general_test.nx -- (#1) the generator GENERALIZED beyond x*C-in-two- 2// terms. It authors an N-term shift/add chain for ANY constant via the non-adjacent 3// form (NAF), the canonical minimal signed-digit recoding (Reitwiesner, IRE Trans. 4// 1960; Booth recoding). NAF gives the fewest +/- shifted terms, so the generator 5// handles constants the 2-term strength-reducer could NOT (x*100, x*11, x*13, ...). 6// Each authored chain is lowered through the SPEC ENCODER (nx_isa_spec) to RV64 AND 7// AArch64 and PROVEN BY EXECUTION on the sovereign emulators. 8// 9// The team authors: I wrote the recoding + the lowering; the search/recoding writes 10// the term sequence and the spec table writes the bytes. Known answer: every 11// constant computes x*C on both arches -> exit 0. 12 13import "nx_isa_spec.nx" 14import "nx_emu_rv64.nx" 15import "nx_emu_arm64.nx" 16 17func g_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 18func g_num(v: i64) -> i64 { 19 let b: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m } 20 let t: *u8 = sys_mmap(28); var k: i64 = 0 21 if m == 0 { t[0] = 48; k = 1 } 22 while m > 0 { t[k] = 48 + (m % 10); m = m / 10; k = k + 1 } 23 var i: i64 = 0; while i < k { b[i] = t[k - 1 - i]; i = i + 1 } 24 sys_write(1, b, k); return 0 25} 26func g_put_w(code: *u8, o: i64, w: i64) -> i64 { 27 code[o] = w & 0xff; code[o+1] = (w >> 8) & 0xff; code[o+2] = (w >> 16) & 0xff; code[o+3] = (w >> 24) & 0xff 28 return o + 4 29} 30 31// THE GENERATOR: non-adjacent form of C -> terms (pos, sign in {+1,-1}). Returns 32// the term count. Minimal Hamming weight among signed-digit forms. 33func g_naf(C: i64, pos: *i64, sign: *i64) -> i64 { 34 var n: i64 = 0 35 var c: i64 = C 36 var i: i64 = 0 37 while c != 0 { 38 if (c & 1) == 1 { 39 let d: i64 = 2 - (c & 3) // c mod 4 == 1 -> +1 ; == 3 -> -1 40 pos[n] = i; sign[n] = d; n = n + 1 41 c = c - d 42 } 43 c = c >> 1 44 i = i + 1 45 } 46 return n 47} 48 49// lower the authored term chain to RV64 (via the spec table), run, return result. 50func g_run_rv(x: i64, pos: *i64, sign: *i64, nt: i64) -> i64 { 51 let code: *u8 = sys_mmap(256); var o: i64 = 0 52 o = g_put_w(code, o, isa_emit(I_RV_ADDI, 11, 0, 0, x)) // li a1, x 53 o = g_put_w(code, o, isa_emit(I_RV_ADDI, 10, 0, 0, 0)) // li a0, 0 54 var k: i64 = 0 55 while k < nt { 56 o = g_put_w(code, o, isa_emit(I_RV_SLLI, 5, 11, 0, pos[k])) // slli t0, a1, pos 57 if sign[k] > 0 { o = g_put_w(code, o, isa_emit(I_RV_ADD, 10, 10, 5, 0)) } 58 else { o = g_put_w(code, o, isa_emit(I_RV_SUB, 10, 10, 5, 0)) } 59 k = k + 1 60 } 61 o = g_put_w(code, o, isa_emit(I_RV_ADDI, 17, 0, 0, 93)) 62 o = g_put_w(code, o, isa_emit(I_RV_ECALL, 0, 0, 0, 0)) 63 return emu_rv64_run(code, o) 64} 65// lower to AArch64 -- the shifted-register add/sub does the shift INLINE (tighter). 66func g_run_a64(x: i64, pos: *i64, sign: *i64, nt: i64) -> i64 { 67 let code: *u8 = sys_mmap(256); var o: i64 = 0 68 o = g_put_w(code, o, isa_emit(I_A64_MOVZ, 1, 0, 0, x)) // movz x1, x 69 o = g_put_w(code, o, isa_emit(I_A64_MOVZ, 0, 0, 0, 0)) // movz x0, 0 70 var k: i64 = 0 71 while k < nt { 72 if sign[k] > 0 { o = g_put_w(code, o, isa_emit(I_A64_ADD, 0, 0, 1, pos[k])) } // add x0,x0,x1,lsl #pos 73 else { o = g_put_w(code, o, isa_emit(I_A64_SUB, 0, 0, 1, pos[k])) } // sub x0,x0,x1,lsl #pos 74 k = k + 1 75 } 76 o = g_put_w(code, o, isa_emit(I_A64_MOVZ, 8, 0, 0, 93)) 77 o = g_put_w(code, o, isa_emit(I_A64_SVC, 0, 0, 0, 0)) 78 return emu_arm64_run(code, o) 79} 80 81func main() -> i64 { 82 g_puts("=== GENERAL multiply superopt (NAF, any constant), spec-lowered, multi-arch ===\n" as *u8) 83 let consts: *i64 = sys_mmap(8 * 16) as *i64 84 var n: i64 = 0 85 consts[n] = 7; n = n + 1 86 consts[n] = 11; n = n + 1 87 consts[n] = 13; n = n + 1 88 consts[n] = 100; n = n + 1 // the 2-term reducer FAILED this; NAF handles it 89 consts[n] = 23; n = n + 1 90 consts[n] = 45; n = n + 1 91 92 let pos: *i64 = sys_mmap(8 * 32) as *i64 93 let sign: *i64 = sys_mmap(8 * 32) as *i64 94 var rv_ok: i64 = 0 95 var a64_ok: i64 = 0 96 var i: i64 = 0 97 while i < n { 98 let C: i64 = consts[i] 99 let nt: i64 = g_naf(C, pos, sign) // GENERATE the term chain 100 let maxx: i64 = 255 / C 101 var rok: i64 = 1 102 var aok: i64 = 1 103 var x: i64 = 0 104 while x <= maxx { 105 if g_run_rv(x, pos, sign, nt) != x * C { rok = 0 } 106 if g_run_a64(x, pos, sign, nt) != x * C { aok = 0 } 107 x = x + 1 108 } 109 g_puts(" x*" as *u8); g_num(C); g_puts(" (" as *u8); g_num(nt); g_puts(" terms) " as *u8) 110 if rok == 1 { rv_ok = rv_ok + 1; g_puts("RV64:exec-ok " as *u8) } else { g_puts("RV64:FAIL " as *u8) } 111 if aok == 1 { a64_ok = a64_ok + 1; g_puts("ARM64:exec-ok\n" as *u8) } else { g_puts("ARM64:FAIL\n" as *u8) } 112 i = i + 1 113 } 114 115 g_puts("----------------------------------------------------------------\n" as *u8) 116 g_puts(" general superopt proven: RV64 " as *u8); g_num(rv_ok); g_puts("/" as *u8); g_num(n) 117 g_puts(" ARM64 " as *u8); g_num(a64_ok); g_puts("/" as *u8); g_num(n); g_puts("\n" as *u8) 118 g_puts(" ANY constant -> NAF term chain -> spec-lowered to two ISAs -> emulator-proven.\n" as *u8) 119 120 if rv_ok != n { sys_exit(1); return 1 } 121 if a64_ok != n { sys_exit(2); return 2 } 122 sys_exit(0) 123 return 0 124}