Expand description
bignum_rtl — the numeric tower’s foundation in silicon: the BigInt datapath.
logicaffeine_base::numeric::BigInt is sign + little-endian u64 limbs; its magnitude
arithmetic (mag_add/mag_sub/mag_cmp/mag_mul) is schoolbook limb work. This module
emits that as synthesizable silicon:
• bigint_alu — a 256-bit (4-limb) add / subtract / unsigned-compare datapath (shared
carry-borrow chain);
• bigint_mul — the 64×64→128 limb multiplier that mag_mul iterates.
Each is proven TWO ways: byte-identical to its software oracle under iverilog (random +
edge vectors), AND — the same bar the flagship ALU meets — correct by our OWN certified
SAT (exhaustive algebraic identities: the adder is a group, the comparator a total order,
the multiplier commutative and distributive over add).
Arbitrary-precision growth and Rational / Decimal / Complex ride the numeric-tower
coprocessor built ON this datapath — roadmap. The full-width 256-bit product is this
bigint_mul primitive composed with the (proven) bigint_alu accumulate, exactly as
mag_mul composes limb products with carry-adds.
Constants§
Functions§
- emit_
bigint_ alu_ testbench - Self-checking ALU testbench: apply N (a,b) and compare sum/cout, diff/borrow, eq/lt against
the software oracle from
bigint_{a,b}.hex+bigint_{sum,sub,cmp}.hex. Prints PASS/FAIL. - emit_
bigint_ alu_ verilog - Emit the 256-bit add / subtract / compare datapath. The
{cout,sum}/{borrow,diff}use a 257-bit context so the carry / borrow out of the top limb is captured;ltis the borrow (a < b ⇔ the subtract underflows),eqthe magnitude equality. - emit_
bigint_ div_ testbench - Emit the divide block’s self-checking testbench: drive
bigint_div, wait fordone, and check quotient+remainder against the native 256-bit unsigneda / b/a % breference over edge cases plus a 2000-pair random sweep. PASS iff all match. - emit_
bigint_ div_ verilog - Emit the BigInt divide block — a sequential 256-bit UNSIGNED long divider (1 bit/cycle restoring,
W cycles) computing q = a / b, r = a % b over magnitudes, b==0 -> q=r=0. The wide analogue of
shared_divider’s magnitude core (no signed fixup — BigInt carries its sign separately); it feeds the numeric-tower BigInt divide the wayshared_dividerfeeds the 32-bit ALU. 4,340 LUT / 1,548 FF on the ECP5-85K. Proven == the reference magnitude division by iverilog (tb_bigint_div) and ==numeric::mag_div’s algorithm by the Rust model test below. - emit_
bigint_ mul_ testbench - Self-checking multiplier testbench: N (a,b) 64-bit, compare
prodagainst(a*b)128-bit. - emit_
bigint_ mul_ verilog - Emit the 64×64→128 limb multiplier (the partial product
mag_mulaccumulates). - limb_
add - The software limb-add — a faithful mirror of
logicaffeine_base::numeric::mag_add(little-endian u64 limbs, u128 carry): the lowLIMBSsum limbs and the carry-out. - limb_lt
- Unsigned magnitude compare — mirror of
mag_cmp(most-significant limb dominates). - limb_
mul - The limb multiply
mag_muliterates: one 64×64→128 partial product. - limb_
sub - The software limb-subtract — mirror of
mag_sub’s borrow chain, but total (defined for every a, b): the lowLIMBSdifference limbs and the borrow-out (1iff a < b, i.e. the subtraction underflowed). Whenborrow == 0the difference equalsmag_sub(a, b). - wdiv256
- The unsigned quotient
a / bover 256-bit magnitudes — binary long division (b==0 → 0), the reference forbigint_div’s restoring loop; the soft-core’sBigIntWideDiv routes to that block. - wmul256
- The low 256 bits of
a * b— schoolbook overLIMBSlimbs, carries past the top limb dropped (the wraparound a fixed 256-bit datapath produces). This isbigint_mul(64×64) composed with the provenbigint_alucarry-adds; the reference for the soft-core’sBigIntWideMul.