code wiki / _hdl_build / nx_recip64_scalar_test.nx
nx_recip64_scalar_test.nx
buildroot/runtime/_hdl_build/nx_recip64_scalar_test.nx
about
nx_recip64_scalar_test.nx -- ALGORITHM-FIRST proof of the true 64-bit unsigned
Newton-Raphson reciprocal divider (the scalar form, before gate-net emission).
Verified bit-exact vs the PROVEN unsigned oracle nx_rv64im_udiv over a hard
battery (dense small + 100k random FULL 64-bit incl. bit-63-set + every power
of two + edges). Once this is 1:1, the gate-net mirrors it.
Method (normalized reciprocal, mulh-only -- no 128-bit datapath needed):
s = 63 - msb(D); Dn = D<<s in [2^63,2^64) (dn = Dn/2^64 in [0.5,1))
X = 2^63 (seed x=1); repeat: dx=mulhu(Dn,X); t=-dx; Xm=mulhu(X,t);
X = (Xm < 2^63) ? Xm<<1 : ALLONES (cap avoids the x->2 overflow)
q = mulhu(N,X) >>logical msb(D); then overflow-aware +/- correction.
Seed x=1 has error <= 1-dn <= 0.5; quadratic Newton -> 6 iters reach 2^-64.
Known answer: "<ok> <total>" with ok==total, exit 0.
dependencies 1 imports · 0 importers
imports: rv64im_min_alu.nx
imported by: nobody (leaf or entry point)
call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown
structs
| none |
consts
| 18 | const NR64_ITERS: i64 = 7 |
| 19 | const NR64_KCORR: i64 = 6 |
| 20 | const NR64_HALF: i64 = 0 - 9223372036854775808 // 2^63 (as the bit pattern) |
functions
| 22 | func nr64_msb(D: i64) -> i64 { // highest set bit of D>=1 (0..63) |
| 28 | func nr64_div(N: i64, D: i64) -> i64 |
| 65 | func _emit_dec(v: i64) -> i64 called by 1: main |
| 73 | func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 } called by 1: main |
| 75 | func main() -> i64 |