nx_alu_divider.nx source

1// nx_alu_divider.nx -- SYNTHESIZE a correct divider as a gate-network (the 2// invention engine's FIRST real hardware invention; closes the SIL-1 stub where 3// the ALU emitter emitted an ADD cell for DIV). 4// 5// There is no DIV cell kind by design -- division must be BUILT from primitives. 6// This synthesizes a restoring divider (MSB-first, `width` stages) into an 7// NxGsim netlist using only SHL/SHR/SUB/LT/XOR/MUX/OR/AND/CONST cells: 8// rem=0, quo=0; for i = width-1 .. 0: 9// rem_in = (rem << 1) | ((a >> i) & 1) 10// ge = !(rem_in < b) 11// rem = ge ? rem_in - b : rem_in 12// quo = quo | (ge << i) 13// The result is a pure combinational network the gate-level sim (nx_nxgate_sim) 14// can verify 1:1 against behavioral a/b -- so the loop can PROVE a correct 15// divider replaces the stub, not just CATCH the stub. (Operands assumed 16// non-negative + small enough that signed LT == unsigned compare; the full 17// 64-bit unsigned compare is a later widening, mechanical.) 18// 19// This is a gate-network GENERATOR -- parameterised by width, it emits the 20// divider; that is the "invention" artifact, distinct from a hand-built netlist. 21// license_tier: ORIGINAL 22 23import "nx_nxgate_sim.nx" 24import "nx_cell_sink.nx" 25 26// append a CONST cell driving a fresh net = `val`; return the net id. 27func div_const(g: *NxGsim, val: i64) -> i64 { 28 let nn: i64 = g.n_nets 29 g.n_nets = nn + 1 30 let nc: i64 = g.n_cells 31 g.cells[nc].kind = NX_GATE_KIND_CONST 32 g.cells[nc].fanout = nn 33 g.cells[nc].f0 = 0 - 1 34 g.cells[nc].f1 = 0 - 1 35 g.cells[nc].f2 = 0 - 1 36 g.cells[nc].val = val 37 g.n_cells = nc + 1 38 return nn 39} 40 41// append a 2-input cell (kind a b) -> fresh net; return the net id. 42func div_op2(g: *NxGsim, kind: i64, a: i64, b: i64) -> i64 { 43 let nn: i64 = g.n_nets 44 g.n_nets = nn + 1 45 let nc: i64 = g.n_cells 46 g.cells[nc].kind = kind 47 g.cells[nc].fanout = nn 48 g.cells[nc].f0 = a 49 g.cells[nc].f1 = b 50 g.cells[nc].f2 = 0 - 1 51 g.cells[nc].val = 0 52 g.n_cells = nc + 1 53 return nn 54} 55 56// append a MUX (sel ? t : f) -> fresh net; return the net id. 57func div_mux(g: *NxGsim, sel: i64, t: i64, f: i64) -> i64 { 58 let nn: i64 = g.n_nets 59 g.n_nets = nn + 1 60 let nc: i64 = g.n_cells 61 g.cells[nc].kind = NX_GATE_KIND_MUX 62 g.cells[nc].fanout = nn 63 g.cells[nc].f0 = sel 64 g.cells[nc].f1 = t 65 g.cells[nc].f2 = f 66 g.cells[nc].val = 0 67 g.n_cells = nc + 1 68 return nn 69} 70 71// Synthesize the restoring divider against a CELL SINK (the canonical form): 72// emits the SAME divider gate-network to either an in-memory NxGsim (Verifier) 73// or a .nxgate text sink (shipping emitter). na (dividend) / nb (divisor) are 74// pre-existing net ids in the sink's space. Writes the remainder net to 75// rem_out[0]; returns the quotient net. Cell order is identical to the legacy 76// NxGsim form below, so MEM-mode netlists are byte-identical (gates unchanged). 77func nx_div_synth_sink(k: *NxCellSink, na: i64, nb: i64, width: i64, rem_out: *i64) -> i64 { 78 let c0: i64 = nx_sink_const(k, 64, 0) 79 let c1: i64 = nx_sink_const(k, 64, 1) 80 var rem: i64 = c0 81 var quo: i64 = c0 82 var i: i64 = width - 1 83 while i >= 0 { 84 let ci: i64 = nx_sink_const(k, 64, i) 85 let shifted: i64 = nx_sink_cell(k, NX_GATE_KIND_SHL, 64, rem, c1, 0 - 1, 2) // rem << 1 86 let abit_sh: i64 = nx_sink_cell(k, NX_GATE_KIND_SHR, 64, na, ci, 0 - 1, 2) // a >> i 87 let abit: i64 = nx_sink_cell(k, NX_GATE_KIND_AND, 64, abit_sh, c1, 0 - 1, 2) // (a>>i) & 1 88 let rem_in: i64 = nx_sink_cell(k, NX_GATE_KIND_OR, 64, shifted, abit, 0 - 1, 2) // (rem<<1) | bit 89 let lt: i64 = nx_sink_cell(k, NX_GATE_KIND_LTU, 64, rem_in, nb, 0 - 1, 2) // rem_in <u b -> 0/1 90 let ge: i64 = nx_sink_cell(k, NX_GATE_KIND_XOR, 64, lt, c1, 0 - 1, 2) // ge = !lt 91 let sub: i64 = nx_sink_cell(k, NX_GATE_KIND_SUB, 64, rem_in, nb, 0 - 1, 2) // rem_in - b 92 let rem_next: i64 = nx_sink_cell(k, NX_GATE_KIND_MUX, 64, ge, sub, rem_in, 3) // ge ? sub : rem_in 93 let qbit: i64 = nx_sink_cell(k, NX_GATE_KIND_SHL, 64, ge, ci, 0 - 1, 2) // ge << i 94 let quo_next: i64 = nx_sink_cell(k, NX_GATE_KIND_OR, 64, quo, qbit, 0 - 1, 2) // quo | qbit 95 rem = rem_next 96 quo = quo_next 97 i = i - 1 98 } 99 rem_out[0] = rem 100 return quo 101} 102 103// Legacy NxGsim entry point -- now a thin MEM-sink wrapper over the canonical 104// nx_div_synth_sink (ONE divider algorithm). Byte-identical netlist to before. 105func nx_div_synth(g: *NxGsim, na: i64, nb: i64, width: i64, rem_out: *i64) -> i64 { 106 let k: *NxCellSink = sys_mmap(64) as *NxCellSink 107 nx_sink_init_mem(k, g) 108 return nx_div_synth_sink(k, na, nb, width, rem_out) 109}