nx_alu_select.nx source

1// nx_alu_select.nx -- THE one ALU op-select builder, written against NxCellSink. 2// 3// Called with a MEM sink it fills an NxGsim the Verifier runs; called with a 4// TEXT sink it emits the .nxgate the shipping synth ships. Same code -> the 5// verifier proves exactly what the emitter ships (one source, two sinks). 6// 7// Topology (per op K in 1..N-1): CONST(K) opcode + subnet + EQ(op_in==K) match; 8// then a cascade MUX(match_K, subnet_K, prev). use_divider=1 makes DIV/DIVU take 9// the PROVEN restoring divider's quotient and REM/REMU its remainder (the first 10// hardware invention, in the shipped ALU); use_divider=0 keeps the single-cell 11// stub from the single-source op->kind map (the baseline that catches holes). 12// 13// na/nb/nop are pre-existing net ids for a / b / op_in in the sink's net space. 14// Returns the cascade result net id (caller wires it to the result port / records 15// it as the sim output). 16 17import "nx_cell_sink.nx" 18import "nx_alu_divider.nx" // nx_div_synth_sink 19import "nx_alu_op_kind.nx" // nx_alu_op_to_gate_kind 20import "rv64im_min_alu.nx" // NX_RV64IM_ALU_* 21import "nx_mul_wide.nx" // nx_mul_wide_sink (high-product for mulh) 22const K_MAGIC_4294967295: i64 = 4294967295 23const K_MAGIC_4294967296: i64 = 4294967296 24 25// sink mulh subnet: high 64 bits of a*b + two's-complement sign corrections. 26// mulhu (0,0) ; mulhsu (1,0) ; mulh (1,1). Matches behavioral nx_rv64im_mulh_*. 27func nx_alu_mulh_sink(k: *NxCellSink, na: i64, nb: i64, do_a: i64, do_b: i64) -> i64 { 28 let hio: *i64 = sys_mmap(8) as *i64 29 hio[0] = 0 30 let lo: i64 = nx_mul_wide_sink(k, na, nb, hio) 31 var hi: i64 = hio[0] 32 let c0: i64 = nx_sink_const(k, 64, 0) 33 if do_a == 1 { 34 let sa: i64 = nx_sink_cell(k, NX_GATE_KIND_LT, 1, na, c0, 0 - 1, 2) 35 let cora: i64 = nx_sink_cell(k, NX_GATE_KIND_MUX, 64, sa, nb, c0, 3) 36 hi = nx_sink_cell(k, NX_GATE_KIND_SUB, 64, hi, cora, 0 - 1, 2) 37 } 38 if do_b == 1 { 39 let sb: i64 = nx_sink_cell(k, NX_GATE_KIND_LT, 1, nb, c0, 0 - 1, 2) 40 let corb: i64 = nx_sink_cell(k, NX_GATE_KIND_MUX, 64, sb, na, c0, 3) 41 hi = nx_sink_cell(k, NX_GATE_KIND_SUB, 64, hi, corb, 0 - 1, 2) 42 } 43 return hi 44} 45 46// sink sign-extend of the low 32 bits (gate form of sext32). 47func nx_sext32_sink(k: *NxCellSink, v: i64) -> i64 { 48 let cmask: i64 = nx_sink_const(k, 64, K_MAGIC_4294967295) 49 let c31: i64 = nx_sink_const(k, 64, 31) 50 let c1: i64 = nx_sink_const(k, 64, 1) 51 let chi: i64 = nx_sink_const(k, 64, 0 - K_MAGIC_4294967296) 52 let c0: i64 = nx_sink_const(k, 64, 0) 53 let low: i64 = nx_sink_cell(k, NX_GATE_KIND_AND, 64, v, cmask, 0 - 1, 2) 54 let sbsh: i64 = nx_sink_cell(k, NX_GATE_KIND_SHR, 64, low, c31, 0 - 1, 2) 55 let sb: i64 = nx_sink_cell(k, NX_GATE_KIND_AND, 64, sbsh, c1, 0 - 1, 2) 56 let fill: i64 = nx_sink_cell(k, NX_GATE_KIND_MUX, 64, sb, chi, c0, 3) 57 return nx_sink_cell(k, NX_GATE_KIND_OR, 64, low, fill, 0 - 1, 2) 58} 59 60// sink W-suffix UNSIGNED div/rem (32-bit operands, sext32 result). 61func nx_wdiv_u_sink(k: *NxCellSink, na: i64, nb: i64, want_rem: i64) -> i64 { 62 let cmask: i64 = nx_sink_const(k, 64, K_MAGIC_4294967295) 63 let c0: i64 = nx_sink_const(k, 64, 0) 64 let a32: i64 = nx_sink_cell(k, NX_GATE_KIND_AND, 64, na, cmask, 0 - 1, 2) 65 let b32: i64 = nx_sink_cell(k, NX_GATE_KIND_AND, 64, nb, cmask, 0 - 1, 2) 66 let ro: *i64 = sys_mmap(8) as *i64 67 ro[0] = 0 68 let q: i64 = nx_div_synth_sink(k, a32, b32, 32, ro) 69 let r: i64 = ro[0] 70 let bz: i64 = nx_sink_cell(k, NX_GATE_KIND_EQ, 1, b32, c0, 0 - 1, 2) 71 if want_rem == 0 { 72 let qse: i64 = nx_sext32_sink(k, q) 73 let allone: i64 = nx_sink_const(k, 64, 0 - 1) 74 return nx_sink_cell(k, NX_GATE_KIND_MUX, 64, bz, allone, qse, 3) 75 } 76 let rse: i64 = nx_sext32_sink(k, r) 77 let ase: i64 = nx_sext32_sink(k, na) 78 return nx_sink_cell(k, NX_GATE_KIND_MUX, 64, bz, ase, rse, 3) 79} 80 81// sink W-suffix SIGNED div/rem (sext32 operands, abs+unsigned-divide+sign-correct). 82func nx_wdiv_s_sink(k: *NxCellSink, na: i64, nb: i64, want_rem: i64) -> i64 { 83 let cmask: i64 = nx_sink_const(k, 64, K_MAGIC_4294967295) 84 let c0: i64 = nx_sink_const(k, 64, 0) 85 let a32: i64 = nx_sext32_sink(k, na) 86 let b32: i64 = nx_sext32_sink(k, nb) 87 let sa: i64 = nx_sink_cell(k, NX_GATE_KIND_LT, 1, a32, c0, 0 - 1, 2) 88 let sb: i64 = nx_sink_cell(k, NX_GATE_KIND_LT, 1, b32, c0, 0 - 1, 2) 89 let aa: i64 = nx_sink_cell(k, NX_GATE_KIND_MUX, 64, sa, nx_sink_cell(k, NX_GATE_KIND_SUB, 64, c0, a32, 0 - 1, 2), a32, 3) 90 let bb: i64 = nx_sink_cell(k, NX_GATE_KIND_MUX, 64, sb, nx_sink_cell(k, NX_GATE_KIND_SUB, 64, c0, b32, 0 - 1, 2), b32, 3) 91 let ro: *i64 = sys_mmap(8) as *i64 92 ro[0] = 0 93 let qu: i64 = nx_div_synth_sink(k, aa, bb, 32, ro) 94 let ru: i64 = ro[0] 95 let qsign: i64 = nx_sink_cell(k, NX_GATE_KIND_XOR, 1, sa, sb, 0 - 1, 2) 96 let q: i64 = nx_sink_cell(k, NX_GATE_KIND_MUX, 64, qsign, nx_sink_cell(k, NX_GATE_KIND_SUB, 64, c0, qu, 0 - 1, 2), qu, 3) 97 let r: i64 = nx_sink_cell(k, NX_GATE_KIND_MUX, 64, sa, nx_sink_cell(k, NX_GATE_KIND_SUB, 64, c0, ru, 0 - 1, 2), ru, 3) 98 let b32low: i64 = nx_sink_cell(k, NX_GATE_KIND_AND, 64, nb, cmask, 0 - 1, 2) 99 let bz: i64 = nx_sink_cell(k, NX_GATE_KIND_EQ, 1, b32low, c0, 0 - 1, 2) 100 if want_rem == 0 { 101 let qse: i64 = nx_sext32_sink(k, q) 102 let allone: i64 = nx_sink_const(k, 64, 0 - 1) 103 return nx_sink_cell(k, NX_GATE_KIND_MUX, 64, bz, allone, qse, 3) 104 } 105 let rse: i64 = nx_sext32_sink(k, r) 106 let ase: i64 = nx_sext32_sink(k, na) 107 return nx_sink_cell(k, NX_GATE_KIND_MUX, 64, bz, ase, rse, 3) 108} 109 110func nx_alu_build_select(k: *NxCellSink, na: i64, nb: i64, nop: i64, use_divider: i64) -> i64 { 111 let sub_nets: *i64 = sys_mmap(8 * NX_RV64IM_ALU_N) as *i64 112 let match_nets: *i64 = sys_mmap(8 * NX_RV64IM_ALU_N) as *i64 113 let rem_out: *i64 = sys_mmap(8) as *i64 114 115 // ----- Phase 1: per-op CONST + subnet + match ----- 116 var op: i64 = 1 117 while op < NX_RV64IM_ALU_N { 118 let c_net: i64 = nx_sink_const(k, 8, op) 119 120 var sub: i64 = 0 - 1 121 if use_divider == 1 { 122 if op == NX_RV64IM_ALU_DIV { sub = nx_div_synth_sink(k, na, nb, 64, rem_out) } 123 if op == NX_RV64IM_ALU_DIVU { sub = nx_div_synth_sink(k, na, nb, 64, rem_out) } 124 if op == NX_RV64IM_ALU_REM { let q: i64 = nx_div_synth_sink(k, na, nb, 64, rem_out); sub = rem_out[0] } 125 if op == NX_RV64IM_ALU_REMU { let q: i64 = nx_div_synth_sink(k, na, nb, 64, rem_out); sub = rem_out[0] } 126 if op == NX_RV64IM_ALU_MULHU { sub = nx_alu_mulh_sink(k, na, nb, 0, 0) } 127 if op == NX_RV64IM_ALU_MULHSU { sub = nx_alu_mulh_sink(k, na, nb, 1, 0) } 128 if op == NX_RV64IM_ALU_MULH { sub = nx_alu_mulh_sink(k, na, nb, 1, 1) } 129 if op == NX_RV64IM_ALU_DIVUW { sub = nx_wdiv_u_sink(k, na, nb, 0) } 130 if op == NX_RV64IM_ALU_REMUW { sub = nx_wdiv_u_sink(k, na, nb, 1) } 131 if op == NX_RV64IM_ALU_DIVW { sub = nx_wdiv_s_sink(k, na, nb, 0) } 132 if op == NX_RV64IM_ALU_REMW { sub = nx_wdiv_s_sink(k, na, nb, 1) } 133 } 134 if sub < 0 { 135 let kind: i64 = nx_alu_op_to_gate_kind(op) 136 if kind >= 0 { 137 // RV64 spec: SLL/SRL/SRA take the shift amount from rs2[5:0] (low 6 bits). Mask the 138 // shift operand at the gate level so out-of-range amounts MATCH the behavioral ALU 139 // (closes the recorded rs2[5:0] shift-mask gap; in-range behavior is unchanged). The 140 // mask cells flow into BOTH the mem-sink verifier AND the shipped .nxgate emitter. 141 var bsh: i64 = nb 142 if op == NX_RV64IM_ALU_SLL { bsh = nx_sink_cell(k, NX_GATE_KIND_AND, 64, nb, nx_sink_const(k, 64, 63), 0 - 1, 2) } 143 if op == NX_RV64IM_ALU_SRL { bsh = nx_sink_cell(k, NX_GATE_KIND_AND, 64, nb, nx_sink_const(k, 64, 63), 0 - 1, 2) } 144 if op == NX_RV64IM_ALU_SRA { bsh = nx_sink_cell(k, NX_GATE_KIND_AND, 64, nb, nx_sink_const(k, 64, 63), 0 - 1, 2) } 145 sub = nx_sink_cell(k, kind, 64, na, bsh, 0 - 1, 2) 146 } 147 } 148 sub_nets[op] = sub 149 150 let m_net: i64 = nx_sink_cell(k, NX_GATE_KIND_EQ, 1, nop, c_net, 0 - 1, 2) 151 match_nets[op] = m_net 152 op = op + 1 153 } 154 155 // ----- Phase 2: cascade MUX ----- 156 var prev: i64 = nx_sink_const(k, 64, 0) 157 op = 1 158 while op < NX_RV64IM_ALU_N { 159 prev = nx_sink_cell(k, NX_GATE_KIND_MUX, 64, match_nets[op], sub_nets[op], prev, 3) 160 op = op + 1 161 } 162 return prev 163}