nx_recip_synth.nx source

1// nx_recip_synth.nx -- the MULTIPLICATIVE (Newton-Raphson reciprocal) divider 2// instantiated as an NxGsim GATE-NETWORK (the gate-network instantiation of the 3// algorithm proven scalar in nx_alu_divider_newton.nx, maxcorr=1). 4// 5// This is the "first provable rung" (W=16): the SAME Newton math as the scalar 6// proof, emitted as a pure combinational word-level netlist using ONLY the 7// already-proven cell builders div_const / div_op2 / div_mux (nx_alu_divider.nx) 8// over the gate-sim's MUL/SHL/SHR/SUB/ADD/LTU/XOR/AND/OR/MUX/CONST cells. 9// 10// WHY W=16 is the smallest GATE-NETWORK-provable variant: 11// At W=16 every intermediate fits i64 with a PLAIN depth-1 MUL cell, so NO 12// nx_mul_wide (128-bit organ) is needed -- verified bit-widths (D<=2^16): 13// dn <= 2^16 (17b) dn*x = dx <= 2^33 (34b) 14// 2F^2-dx = t <= 2^33 (34b) x*t <= 2^49 (49b) 15// N*x <= 2^33 (34b) 16// all <= 49 bits, so a single MUL cell (low 64 bits, no wrap) is EXACT here. 17// The new code is therefore just the gate-emitter wrapper around 100%-proven 18// math + proven cells -- no new unproven gate organ is exercised. The 19// nx_mul_wide-dependent rungs (W>=24, x*t=73b) are the next milestone. 20// 21// data-dependent normalization (msb_pos / barrel-shift) is BUILT IN GATES here: 22// - msb_synth : priority encoder over a runtime net (cascade of LTU/MUX), 23// returns p with 2^p <= D < 2^(p+1) for D in [1, 2^16). 24// - barrel SHL/SHR by a *net* count uses the sim's SHL/SHR cells directly 25// (the cell takes b = the runtime shift-count net), so normalization 26// Dn = D<<s and extraction (N*x)>>(17+p) are pure gates. 27// 28// The correction tail is UNROLLED to a fixed KCORR (data-INDEPENDENT, so the 29// latency stays O(iters)+O(1)); the scalar proof showed maxcorr=1, so KCORR=2 30// is a safe constant. license_tier: ORIGINAL 31// 32// HONEST-METRIC NOTE (do not fool ourselves): nx_nxgate_sim assigns depth-1 to 33// every word-level cell, so a MUL cell looks as cheap as an AND. This proves 34// FUNCTIONAL 1:1 correctness of the gate-network, and the iteration COUNT 35// (3 vs W=16 restoring stages) is a real cell-count/sequential-step win -- but 36// NOT a true critical-path latency exceed until a real gate-delay model exists. 37 38import "nx_mul_wide.nx" 39 40const RS_W: i64 = 16 41const RS_F: i64 = 65536 // 2^16 fixed-point scale (Q16) 42const RS_FF2: i64 = 8589934592 // 2 * F * F = 2^33 43const RS_ITERS: i64 = 3 // matches the proven scalar NW_ITERS 44const RS_KCORR: i64 = 2 // unrolled correction stages (proven maxcorr=1) 45 46// ----- msb_synth: priority encoder as gates ---------------------------------- 47// returns a NET whose value is p with 2^p <= D < 2^(p+1), for D in [1, 2^RS_W). 48// Built as a cascade: p = sum over k in 1..W-1 of (D >= 2^k ? 1 : 0) 49// ge_k = !(D <u 2^k) = (D <u 2^k) XOR 1 50// p = p + ge_k 51// For D=0 this returns 0 (matches the scalar msb_pos(0)=0 fall-through; the 52// caller's correction tail + the test's D>=1 keep this path unexercised, but it 53// is defined, not undefined). Topological order is preserved (each cell's fanins 54// are already-built nets). 55func msb_synth(g: *NxGsim, nd: i64) -> i64 { 56 let c1: i64 = div_const(g, 1) 57 var p: i64 = div_const(g, 0) 58 var k: i64 = 1 59 while k < RS_W { 60 let pow: i64 = div_const(g, 1 << k) // 2^k 61 let lt: i64 = div_op2(g, NX_GATE_KIND_LTU, nd, pow) // D <u 2^k 62 let ge: i64 = div_op2(g, NX_GATE_KIND_XOR, lt, c1) // D >= 2^k ? 1 : 0 63 p = div_op2(g, NX_GATE_KIND_ADD, p, ge) // accumulate 64 k = k + 1 65 } 66 return p 67} 68 69// ----- recip_const_div17: exact integer floor(num/17) as a gate-network ------- 70// 17 is a compile-time constant, so this is a fixed restoring divide-by-17 71// network (no divider-in-the-divider). num <= 48*65536 = 3145728 < 2^22, so 22 72// MSB-first restoring stages give the exact floor. Pure SHL/SHR/AND/OR/LTU/XOR/ 73// SUB/MUX/CONST -- the same proven primitives as nx_alu_divider's restoring core. 74func recip_const_div17(g: *NxGsim, num: i64) -> i64 { 75 let c0: i64 = div_const(g, 0) 76 let c1: i64 = div_const(g, 1) 77 let c17: i64 = div_const(g, 17) 78 var rem: i64 = c0 79 var quo: i64 = c0 80 var i: i64 = 22 - 1 81 while i >= 0 { 82 let ci: i64 = div_const(g, i) 83 let sh: i64 = div_op2(g, NX_GATE_KIND_SHL, rem, c1) // rem << 1 84 let absh: i64 = div_op2(g, NX_GATE_KIND_SHR, num, ci) // num >> i 85 let abit: i64 = div_op2(g, NX_GATE_KIND_AND, absh, c1) // (num>>i)&1 86 let remin: i64 = div_op2(g, NX_GATE_KIND_OR, sh, abit) // (rem<<1)|bit 87 let lt: i64 = div_op2(g, NX_GATE_KIND_LTU, remin, c17) // remin <u 17 88 let ge: i64 = div_op2(g, NX_GATE_KIND_XOR, lt, c1) // !lt 89 let sub: i64 = div_op2(g, NX_GATE_KIND_SUB, remin, c17) // remin-17 90 let remn: i64 = div_mux(g, ge, sub, remin) 91 let qbit: i64 = div_op2(g, NX_GATE_KIND_SHL, ge, ci) // ge<<i 92 let quon: i64 = div_op2(g, NX_GATE_KIND_OR, quo, qbit) 93 rem = remn 94 quo = quon 95 i = i - 1 96 } 97 return quo 98} 99 100// ----- nx_recip_div_synth: Newton reciprocal divider as a gate-network -------- 101// Builds the network for nets na (dividend) / nb (divisor) at W=16. 102// Writes the remainder net id to rem_out[0]; returns the quotient net id. 103// Mirrors nw_div() in nx_alu_divider_newton.nx exactly, op for op. 104func nx_recip_div_synth(g: *NxGsim, na: i64, nb: i64, rem_out: *i64) -> i64 { 105 let c1: i64 = div_const(g, 1) 106 let cF48: i64 = div_const(g, 48 * RS_F) // 48F (compile-folded const) 107 let c32: i64 = div_const(g, 32) 108 let c17: i64 = div_const(g, 17) 109 let cFF2: i64 = div_const(g, RS_FF2) // 2F^2 = 2^33 110 let cWm1: i64 = div_const(g, RS_W - 1) // W-1 = 15 111 let cWp1: i64 = div_const(g, RS_W + 1) // W+1 = 17 112 113 // --- normalize: p=msb(D), s=(W-1)-p, dn=D<<s (dn in [F/2,F)) --- 114 let p: i64 = msb_synth(g, nb) 115 let s: i64 = div_op2(g, NX_GATE_KIND_SUB, cWm1, p) // s = 15 - p 116 let dn: i64 = div_op2(g, NX_GATE_KIND_SHL, nb, s) // Dn = D << s 117 118 // --- minimax linear seed x0 = (48F - 32*Dn)/17 (Q16) --- 119 // The scalar uses /17, a CONSTANT divide. There is no DIV cell kind by design, 120 // and 1/17 ~ 3855/2^16 truncation perturbs the 4-bit seed enough that the W=16 121 // Newton+KCORR budget can break on some divisors -- so we synthesize the EXACT 122 // integer floor(num/17) as a tiny restoring divide-by-constant network 123 // (recip_const_div17, defined above; 17 is a compile-time constant => fixed gates). 124 let t32: i64 = div_op2(g, NX_GATE_KIND_MUL, c32, dn) // 32*Dn (<= 2^21) 125 let num: i64 = div_op2(g, NX_GATE_KIND_SUB, cF48, t32) // 48F - 32Dn 126 var x: i64 = recip_const_div17(g, num) // EXACT floor(num/17) 127 128 // --- Newton: x = (x*(2F^2 - Dn*x)) >> 32, RS_ITERS times --- 129 var it: i64 = 0 130 while it < RS_ITERS { 131 let dx: i64 = div_op2(g, NX_GATE_KIND_MUL, dn, x) // Dn*x (<= 2^33) 132 let t: i64 = div_op2(g, NX_GATE_KIND_SUB, cFF2, dx) // 2F^2 - Dn*x 133 let xt: i64 = div_op2(g, NX_GATE_KIND_MUL, x, t) // x*t (<= 2^49) 134 x = div_op2(g, NX_GATE_KIND_SHR, xt, c32) // >> 32 135 it = it + 1 136 } 137 138 // --- quotient extraction: q = (N*x) >> (17 + p) --- 139 let nx: i64 = div_op2(g, NX_GATE_KIND_MUL, na, x) // N*x (<= 2^33) 140 let amt: i64 = div_op2(g, NX_GATE_KIND_ADD, cWp1, p) // 17 + p 141 var q: i64 = div_op2(g, NX_GATE_KIND_SHR, nx, amt) // >> (17+p) 142 143 // --- UNROLLED O(1) correction (KCORR fixed stages; proven maxcorr=1) --- 144 // each stage: if (q+1)*D <= N -> q+1 ; else if q*D > N -> q-1 ; else q 145 var kc: i64 = 0 146 while kc < RS_KCORR { 147 let qp1: i64 = div_op2(g, NX_GATE_KIND_ADD, q, c1) // q+1 148 let qp1D: i64 = div_op2(g, NX_GATE_KIND_MUL, qp1, nb) // (q+1)*D 149 // (q+1)*D <= N <=> !(N <u (q+1)*D) 150 let nlt: i64 = div_op2(g, NX_GATE_KIND_LTU, na, qp1D) // N <u (q+1)*D 151 let le: i64 = div_op2(g, NX_GATE_KIND_XOR, nlt, c1) // (q+1)*D <= N ? 1 : 0 152 let qD: i64 = div_op2(g, NX_GATE_KIND_MUL, q, nb) // q*D 153 let high: i64 = div_op2(g, NX_GATE_KIND_LTU, na, qD) // q*D > N (N <u q*D) 154 let qup: i64 = div_op2(g, NX_GATE_KIND_ADD, q, le) // q + le 155 let qdn: i64 = div_op2(g, NX_GATE_KIND_SUB, q, high) // q - high 156 // le and high are mutually exclusive, so order is safe: 157 q = div_mux(g, le, qup, div_mux(g, high, qdn, q)) 158 kc = kc + 1 159 } 160 161 // --- remainder: r = N - q*D --- 162 let qDf: i64 = div_op2(g, NX_GATE_KIND_MUL, q, nb) 163 let r: i64 = div_op2(g, NX_GATE_KIND_SUB, na, qDf) 164 rem_out[0] = r 165 return q 166}