Skip to main content

Module bignum_rtl

Module bignum_rtl 

Source
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§

LIMBS

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; lt is the borrow (a < b ⇔ the subtract underflows), eq the magnitude equality.
emit_bigint_div_testbench
Emit the divide block’s self-checking testbench: drive bigint_div, wait for done, and check quotient+remainder against the native 256-bit unsigned a / b / a % b reference 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 way shared_divider feeds 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 prod against (a*b) 128-bit.
emit_bigint_mul_verilog
Emit the 64×64→128 limb multiplier (the partial product mag_mul accumulates).
limb_add
The software limb-add — a faithful mirror of logicaffeine_base::numeric::mag_add (little-endian u64 limbs, u128 carry): the low LIMBS sum limbs and the carry-out.
limb_lt
Unsigned magnitude compare — mirror of mag_cmp (most-significant limb dominates).
limb_mul
The limb multiply mag_mul iterates: 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 low LIMBS difference limbs and the borrow-out (1 iff a < b, i.e. the subtraction underflowed). When borrow == 0 the difference equals mag_sub(a, b).
wdiv256
The unsigned quotient a / b over 256-bit magnitudes — binary long division (b==0 → 0), the reference for bigint_div’s restoring loop; the soft-core’s BigIntWide Div routes to that block.
wmul256
The low 256 bits of a * b — schoolbook over LIMBS limbs, carries past the top limb dropped (the wraparound a fixed 256-bit datapath produces). This is bigint_mul (64×64) composed with the proven bigint_alu carry-adds; the reference for the soft-core’s BigIntWide Mul.