Module simd 

simd — configurable-precision packed SIMD lanes for the fabric datapath (FabricTarget::simd).

HiVec’s TOPS/W comes from packing several narrow lanes into one datapath. Our analog packs lanes values of width bits into the existing 64-bit word and operates lane-wise. The one thing that must never happen is a carry bleeding across a lane boundary — the “silent SIMD integer miscompile”. So the packed hardware op is defined here as an explicit SWAR (SIMD-within-a-register) form built from the fabric’s own AluOp tiles, and simd_tile_lock proves it BIT-IDENTICAL to a lane-wise reference (N independent scalar ops) for ALL 64-bit inputs via our certified SAT. The reference is the spec; the SWAR form is what silicon runs.

Enums

LaneTy

A packed lane type: lanes values of width bits, lanes * width == 64.

VecOp

A packed integer SIMD operation carried by a LoopCell::VectorArith / CellKind::Simd tile. Add is the carry-isolated SWAR add (proven ≡ lane-wise by simd_tile_lock); the bitwise ops never cross a lane boundary, so they are the native 64-bit op.

Constants

FP16_ADD_V

The synthesizable combinational IEEE-754 f16 (binary16) adder — the f32 adder narrowed to 5-bit exponent, 10-bit mantissa, bias 15 (window 128-bit, LSB0=64, leading-ref=74, normalize-target=13). Proven bit-exact to the f16_add reference under iverilog; instantiated once per lane by the packed F16×4 tile.

FP16_MUL_V

The synthesizable combinational IEEE-754 f16 multiplier — the f32 multiplier narrowed to binary16 (11-bit significand product = 22 bits, leading at 20/21). Proven bit-exact to f16_mul under iverilog.

FP32_ADD_V

The synthesizable combinational IEEE-754 f32 adder — a faithful port of the PROVEN f64 fp_addsub (benchmarks/silicon/fpu.v): align both significands in a wide 128-bit window (64 bits of alignment room, so every bit survives to sticky), add/sub, leading-zero-count, normalize the leading 1 to bit 26 (24-bit significand at [26:3], guard/round/sticky at [2:0]), round-to-nearest-ties-even, and pack (overflow→Inf, underflow→subnormal via pack_sub32). sub=1 computes a-b. Proven bit-exact to Rust f32 under iverilog by simd_float_rtl_lock. This module is instantiated once per lane by the packed F32×2 tile.

FP32_MUL_V

The synthesizable combinational IEEE-754 f32 multiplier — a faithful port of the proven f64 fp_mul: pre-normalize each significand (leading 1 to bit 23), multiply (24×24=48-bit, leading at 46/47), normalize the leading 1 to bit 47, round-to-nearest-ties-even, and pack (overflow→Inf, underflow→subnormal, rounded once from the EXACT product to avoid double-rounding). Proven bit-exact to Rust f32 under iverilog.

Functions

emit_fp32_scalar_add_testbench

A self-checking combinational testbench for the scalar fp32_add: drive n (a,b) 32-bit vectors from fp32_add_a.hex/_b.hex, compare the settled y against Rust’s f32 add oracle in fp32_add_o.hex.

emit_fp32_scalar_mul_testbench

A self-checking combinational testbench for the scalar fp32_mul: drive n (a,b) vectors, compare y against Rust’s f32 multiply oracle in fp32_mul_o.hex.

emit_simd_add_testbench

A self-checking combinational testbench for simd_{name}: drive n (a,b) vectors from simd_{name}_a.hex/_b.hex, compare the settled r against the lane-wise oracle in _o.hex, print PASS.

emit_simd_add_verilog

Emit the packed SWAR add as a COMBINATIONAL Verilog module — the SIMD tile the RTL flow tapes out: r = ((a & M) + (b & M)) ^ ((a ^ b) & ~M), one datapath op, carry blocked at every lane boundary. Proven ≡ the lane-wise spec under iverilog by simd_rtl_lock (and ≡ N scalar adds by SAT in simd_tile_lock).

emit_simd_fadd_f16x4_verilog

Emit the packed F16×4 add tile: four fp16_add lanes over the 64-bit operands. Module simd_fadd_f16x4 (ports a,b,r). Compile alongside FP16_ADD_V; proven ≡ eval_lanewise_fadd_f16x4 under iverilog.

emit_simd_fadd_f32x2_verilog

Emit the packed F32×2 add tile: two fp32_add lanes (low = bits [31:0], high = [63:32]) driven in parallel from the 64-bit operands. Module name simd_fadd_f32x2 (ports a,b,r), so the standard SIMD testbench drives it. Compile alongside FP32_ADD_V; proven ≡ eval_lanewise_fadd_f32x2 under iverilog.

emit_simd_fmul_f16x4_verilog

Emit the packed F16×4 multiply tile: four fp16_mul lanes. Module simd_fmul_f16x4. Compile alongside FP16_MUL_V; proven ≡ eval_lanewise_fmul_f16x4 under iverilog.

emit_simd_fmul_f32x2_verilog

Emit the packed F32×2 multiply tile: two fp32_mul lanes in parallel. Module name simd_fmul_f32x2. Compile alongside FP32_MUL_V; proven ≡ eval_lanewise_fmul_f32x2 under iverilog.

eval_lanewise_add

Evaluate the lane-wise add SPEC concretely (each lane an independent width-bit wrapping add).

eval_lanewise_fadd_f16x4

Packed-float add for F16×4 — the SPEC: four independent scalar binary16 adds. Lanes are isolated (a NaN/Inf/subnormal in one cannot perturb another); the parallel fp16 FPU lanes realize it in silicon.

eval_lanewise_fadd_f32x2

Packed-float add for F32×2 (two IEEE-754 f32 lanes in one 64-bit word, lane 0 low) — the SPEC: each lane an independent scalar f32 add. A NaN/Inf/subnormal in one lane cannot perturb the other; SAT cannot bitblast IEEE arithmetic, so simd_tile_lock certifies this by per-lane bit-exactness + a cross-lane non-contamination battery (the way the scalar float lane is already proven). This is the model the parallel fp32 FPU lanes realize in silicon.

eval_lanewise_fmul_f16x4

Packed-float multiply for F16×4 (see eval_lanewise_fadd_f16x4).

eval_lanewise_fmul_f32x2

Packed-float multiply for F32×2 (see eval_lanewise_fadd_f32x2).

f16_add

One correctly-rounded IEEE-754 binary16 add: widen (exact), add in f32 (exact — the sum of two f16s fits in f32’s 24-bit significand), round back RNE. Equals the native binary16 add bit-for-bit (both correctly rounded).

f16_mul

One correctly-rounded IEEE-754 binary16 multiply (see f16_add; the product of two f16s is exact in f32).

f16_to_f32

Widen an IEEE-754 binary16 bit pattern to f32 — EXACT (every f16 value is representable in f32).

f32_to_f16

Round an f32 to an IEEE-754 binary16 bit pattern, round-to-nearest-ties-even (overflow→Inf, underflow→subnormal/0, NaN→canonical qNaN). The one rounding step in the f16 reference; anchored by known-value assertions in simd_tile_lock.

lanewise_add_body

The LANE-WISE reference for packed add — the SPEC: each lane independently computes (a_j + b_j) mod 2^w, expressed as an AluOp residual (shift the lane down, add, mask to width, shift back, OR the lanes). This is “N independent scalar adds” made concrete.

naive_add_body

A deliberately NAIVE (non-isolated) packed add — a single 64-bit add. Carry bleeds across lane boundaries, so it must NOT equal the lane-wise spec (the non-vacuity witness for the isolation proof).

pack_f16x4

Pack four f16 lanes into a 64-bit word (lane 0 low).

pack_f32x2

Pack two f32 lanes into one 64-bit word (lane 0 low).

swar_add_body

The PACKED SWAR add — one datapath op that blocks carry at every lane boundary: ((a & M) + (b & M)) ^ ((a ^ b) & ~M), where M clears each lane’s top bit. This is what the SIMD tile emits; simd_tile_lock certifies it equals lanewise_add_body.