nx_alu_netlist_build_div.nx source

1// nx_alu_netlist_build_div.nx -- the ALU op-select netlist with the PROVEN 2// restoring divider (nx_div_synth) wired into the DIV/DIVU/REM/REMU subnets, 3// in place of the ADD stub. This is the loop's FIRST hardware invention 4// COMPOSED into context: the Generator (nx_div_synth) emits a divider gate- 5// network, the Verifier (nx_gsim_run) proves it matches behavioral div/rem 6// INSIDE the full ALU op-select cascade -- not just in isolation. 7// 8// Same topology as nx_alu_netlist_build (CONST opcode + subnet + EQ match; 9// cascade MUX), built in nx_nxgate_sim's append convention (div_const/div_op2/ 10// div_mux from nx_alu_divider.nx) so the divider sub-network slots in directly. 11// Non-div ops still use the SINGLE-SOURCE nx_alu_op_to_gate_kind (one cell). 12// DIV/DIVU take the divider's quotient; REM/REMU take its remainder. 13// 14// Width 64 (full RV64). Operands assumed non-negative + small enough that the 15// signed LT in the restoring loop equals the unsigned compare -- the documented 16// V1 envelope of nx_div_synth; the full 64-bit unsigned widening is mechanical. 17 18import "nx_alu_netlist_build.nx" // NxAluNetlist, NX_ALUNL_*, nx_alu_op_to_gate_kind 19import "nx_alu_divider.nx" // div_const / div_op2 / div_mux / nx_div_synth 20import "rv64im_min_alu.nx" 21import "nx_mul_wide.nx" // nx_mul_wide_synth (high-product for mulh) 22const NX_MAGIC_4294967295: i64 = 4294967295 23const NX_MAGIC_4294967296: i64 = 4294967296 24 25const NX_ALU_DIV_WIDTH: i64 = 64 26 27// mulh subnet: high 64 bits of a*b, with two's-complement sign corrections. 28// mulhu = hi(a*b) (do_a=0, do_b=0) 29// mulhsu = hi - (a<0 ? b : 0) (do_a=1, do_b=0) 30// mulh = hi - (a<0 ? b : 0) - (b<0 ? a : 0) (do_a=1, do_b=1) 31// a<0 via signed LT against 0 -- matches behavioral nx_rv64im_mulh_*. 32func nxnl_mulh(g: *NxGsim, na: i64, nb: i64, do_a: i64, do_b: i64) -> i64 { 33 let hio: *i64 = sys_mmap(8) as *i64 34 hio[0] = 0 35 let lo: i64 = nx_mul_wide_synth(g, na, nb, hio) 36 var hi: i64 = hio[0] 37 let c0: i64 = div_const(g, 0) 38 if do_a == 1 { 39 let sa: i64 = div_op2(g, NX_GATE_KIND_LT, na, c0) 40 let cora: i64 = div_mux(g, sa, nb, c0) 41 hi = div_op2(g, NX_GATE_KIND_SUB, hi, cora) 42 } 43 if do_b == 1 { 44 let sb: i64 = div_op2(g, NX_GATE_KIND_LT, nb, c0) 45 let corb: i64 = div_mux(g, sb, na, c0) 46 hi = div_op2(g, NX_GATE_KIND_SUB, hi, corb) 47 } 48 return hi 49} 50 51// sign-extend the low 32 bits of v across bits 63..32 (gate form of sext32). 52func nxnl_sext32(g: *NxGsim, v: i64) -> i64 { 53 let cmask: i64 = div_const(g, NX_MAGIC_4294967295) // 0xffffffff 54 let c31: i64 = div_const(g, 31) 55 let c1: i64 = div_const(g, 1) 56 let chi: i64 = div_const(g, 0 - NX_MAGIC_4294967296) // 0xFFFFFFFF00000000 57 let c0: i64 = div_const(g, 0) 58 let low: i64 = div_op2(g, NX_GATE_KIND_AND, v, cmask) 59 let sbsh: i64 = div_op2(g, NX_GATE_KIND_SHR, low, c31) 60 let sb: i64 = div_op2(g, NX_GATE_KIND_AND, sbsh, c1) // bit 31 61 let fill: i64 = div_mux(g, sb, chi, c0) 62 return div_op2(g, NX_GATE_KIND_OR, low, fill) 63} 64 65// W-suffix UNSIGNED divide/remainder: operate on the low 32 bits, sign-extend the 66// 32-bit result. want_rem=0 -> DIVUW (b32==0 -> all-ones); want_rem=1 -> REMUW 67// (b32==0 -> sext32(a)). The 32-bit operands are non-negative so the restoring 68// divider's signed-LT == unsigned-compare envelope holds. 69func nxnl_wdiv_u(g: *NxGsim, na: i64, nb: i64, want_rem: i64) -> i64 { 70 let cmask: i64 = div_const(g, NX_MAGIC_4294967295) 71 let c0: i64 = div_const(g, 0) 72 let a32: i64 = div_op2(g, NX_GATE_KIND_AND, na, cmask) 73 let b32: i64 = div_op2(g, NX_GATE_KIND_AND, nb, cmask) 74 let ro: *i64 = sys_mmap(8) as *i64 75 ro[0] = 0 76 let q: i64 = nx_div_synth(g, a32, b32, 32, ro) 77 let r: i64 = ro[0] 78 let bz: i64 = div_op2(g, NX_GATE_KIND_EQ, b32, c0) // b32 == 0 79 if want_rem == 0 { 80 let qse: i64 = nxnl_sext32(g, q) 81 let allone: i64 = div_const(g, 0 - 1) 82 return div_mux(g, bz, allone, qse) 83 } 84 let rse: i64 = nxnl_sext32(g, r) 85 let ase: i64 = nxnl_sext32(g, na) 86 return div_mux(g, bz, ase, rse) 87} 88 89// W-suffix SIGNED divide/remainder: sext32 the operands, divide magnitudes 90// unsigned, sign-correct (quotient sign = sign(a)^sign(b); remainder sign = 91// sign(a)), sign-extend. want_rem=0 -> DIVW (b32==0 -> all-ones); want_rem=1 -> 92// REMW (b32==0 -> sext32(a)). The abs-then-unsigned-divide naturally yields the 93// RV overflow result (INT_MIN/-1 -> sext32(2^31) = INT_MIN), so no special case. 94func nxnl_wdiv_s(g: *NxGsim, na: i64, nb: i64, want_rem: i64) -> i64 { 95 let cmask: i64 = div_const(g, NX_MAGIC_4294967295) 96 let c0: i64 = div_const(g, 0) 97 let a32: i64 = nxnl_sext32(g, na) 98 let b32: i64 = nxnl_sext32(g, nb) 99 let sa: i64 = div_op2(g, NX_GATE_KIND_LT, a32, c0) // a < 0 100 let sb: i64 = div_op2(g, NX_GATE_KIND_LT, b32, c0) // b < 0 101 let aa: i64 = div_mux(g, sa, div_op2(g, NX_GATE_KIND_SUB, c0, a32), a32) // |a| 102 let bb: i64 = div_mux(g, sb, div_op2(g, NX_GATE_KIND_SUB, c0, b32), b32) // |b| 103 let ro: *i64 = sys_mmap(8) as *i64 104 ro[0] = 0 105 let qu: i64 = nx_div_synth(g, aa, bb, 32, ro) 106 let ru: i64 = ro[0] 107 let qsign: i64 = div_op2(g, NX_GATE_KIND_XOR, sa, sb) 108 let q: i64 = div_mux(g, qsign, div_op2(g, NX_GATE_KIND_SUB, c0, qu), qu) 109 let r: i64 = div_mux(g, sa, div_op2(g, NX_GATE_KIND_SUB, c0, ru), ru) 110 let b32low: i64 = div_op2(g, NX_GATE_KIND_AND, nb, cmask) 111 let bz: i64 = div_op2(g, NX_GATE_KIND_EQ, b32low, c0) 112 if want_rem == 0 { 113 let qse: i64 = nxnl_sext32(g, q) 114 let allone: i64 = div_const(g, 0 - 1) 115 return div_mux(g, bz, allone, qse) 116 } 117 let rse: i64 = nxnl_sext32(g, r) 118 let ase: i64 = nxnl_sext32(g, na) 119 return div_mux(g, bz, ase, rse) 120} 121 122func nx_alu_netlist_build_div(g: *NxGsim, info: *NxAluNetlist) -> i64 { 123 let sub_nets: *i64 = sys_mmap(8 * NX_RV64IM_ALU_N) as *i64 124 let match_nets: *i64 = sys_mmap(8 * NX_RV64IM_ALU_N) as *i64 125 let rem_out: *i64 = sys_mmap(8) as *i64 126 127 g.n_nets = 3 // 0=a 1=b 2=op_in primary inputs 128 g.n_cells = 0 129 130 // ----- Phase 1: per-op CONST + subnet + match ----- 131 var op: i64 = 1 132 while op < NX_RV64IM_ALU_N { 133 let c_net: i64 = div_const(g, op) 134 135 var sub: i64 = 0 - 1 136 // div/rem family: emit the PROVEN divider, take quotient or remainder. 137 if op == NX_RV64IM_ALU_DIV { sub = nx_div_synth(g, NX_ALUNL_A, NX_ALUNL_B, NX_ALU_DIV_WIDTH, rem_out) } 138 if op == NX_RV64IM_ALU_DIVU { sub = nx_div_synth(g, NX_ALUNL_A, NX_ALUNL_B, NX_ALU_DIV_WIDTH, rem_out) } 139 if op == NX_RV64IM_ALU_REM { let q: i64 = nx_div_synth(g, NX_ALUNL_A, NX_ALUNL_B, NX_ALU_DIV_WIDTH, rem_out); sub = rem_out[0] } 140 if op == NX_RV64IM_ALU_REMU { let q: i64 = nx_div_synth(g, NX_ALUNL_A, NX_ALUNL_B, NX_ALU_DIV_WIDTH, rem_out); sub = rem_out[0] } 141 // mulh family: high 64 bits via the PROVEN wide multiplier + sign corrections. 142 if op == NX_RV64IM_ALU_MULHU { sub = nxnl_mulh(g, NX_ALUNL_A, NX_ALUNL_B, 0, 0) } 143 if op == NX_RV64IM_ALU_MULHSU { sub = nxnl_mulh(g, NX_ALUNL_A, NX_ALUNL_B, 1, 0) } 144 if op == NX_RV64IM_ALU_MULH { sub = nxnl_mulh(g, NX_ALUNL_A, NX_ALUNL_B, 1, 1) } 145 // W-suffix unsigned div/rem: 32-bit divide + sign-extend. 146 if op == NX_RV64IM_ALU_DIVUW { sub = nxnl_wdiv_u(g, NX_ALUNL_A, NX_ALUNL_B, 0) } 147 if op == NX_RV64IM_ALU_REMUW { sub = nxnl_wdiv_u(g, NX_ALUNL_A, NX_ALUNL_B, 1) } 148 // W-suffix signed div/rem. 149 if op == NX_RV64IM_ALU_DIVW { sub = nxnl_wdiv_s(g, NX_ALUNL_A, NX_ALUNL_B, 0) } 150 if op == NX_RV64IM_ALU_REMW { sub = nxnl_wdiv_s(g, NX_ALUNL_A, NX_ALUNL_B, 1) } 151 // everything else: single cell from the single-source kind map. 152 if sub < 0 { 153 let kind: i64 = nx_alu_op_to_gate_kind(op) 154 if kind >= 0 { sub = div_op2(g, kind, NX_ALUNL_A, NX_ALUNL_B) } 155 } 156 sub_nets[op] = sub 157 158 let m_net: i64 = div_op2(g, NX_GATE_KIND_EQ, NX_ALUNL_OPIN, c_net) 159 match_nets[op] = m_net 160 op = op + 1 161 } 162 163 // ----- Phase 2: cascade MUX ----- 164 var prev: i64 = div_const(g, 0) 165 op = 1 166 while op < NX_RV64IM_ALU_N { 167 prev = div_mux(g, match_nets[op], sub_nets[op], prev) 168 op = op + 1 169 } 170 171 info.n_cells = g.n_cells 172 info.n_nets = g.n_nets 173 info.result = prev 174 return 0 175}