Module keccak_rtl 

keccak_rtl — the flagship silicon FACT.

The handout’s Keccak throughput was a “design point.” This module makes it real: an iterative Keccak-f[1600] core (one round/cycle, 24-cycle permutation) emitted as synthesizable Verilog whose round function is generated FROM THE SAME θ/ρ+π/χ/ι constants the proven-fast native kernel uses (logicaffeine_system::keccak:: keccak_f1600), so the two cannot diverge by transcription. The RTL is checked bit-exact against the real 24-round oracle under iverilog, synthesized to real ECP5 numbers, and two of its layers are proven by our own certified SAT (θ is GF(2)-linear; χ is a bijection on a row). Plus the ML-KEM NTT butterfly (Montgomery fqmul) emitted, oracle-checked, and its Montgomery invariant SAT-proven.

Structs

NttCuts

Where the pipelined butterfly’s registers go: self.0[i] puts one after step i (NTT_STEPS). The operands and the results are always registered.

Constants

KYBER_Q

q and Montgomery constant — identical to logicaffeine_system::ntt.

KYBER_QINV_I16

NTT_STEPS

The steps of emit_ntt_butterfly_pipelined_verilog’s datapath a register may follow: the four levels of the product’s adder tree; m’s high-byte correction; m; the two partial sums of 13·m + (m >>> 8); that sum; t.

RC

The 24 Keccak-f round constants (FIPS-202) — same table as the native kernel.

Functions

emit_keccak_core_half_verilog

Emit keccak_core_half: the iterative core with a register between theta and the rest of each round, two clocks a round (48 for the permutation), each half carrying only its own wiring — theta’s column parities, then rho and pi’s lane moves into chi. The same ports and handshake as keccak_core.

emit_keccak_core_verilog

Emit the clocked iterative core: start latches s_in, then one round/cycle for 24 cycles applying RC[round]; done pulses with s_out = the permutation result.

emit_keccak_round_verilog

Emit the combinational one-round Keccak-f[1600] module: state s + round constant rc → o. Lane i occupies bits [64*i +: 64] (little-endian lane packing).

emit_keccak_testbench

Self-checking testbench: load the input state + the oracle’s 24-round output from keccak_vec.hex (50 × 64-bit words: 25 input lanes then 25 expected lanes), run the core, compare bit-exact. Prints PASS/FAIL.

emit_keccak_top_verilog

Emit a NARROW-BUS wrapper around keccak_core so it place-and-routes on a real FPGA: the bare core exposes a 1600-bit parallel state port (fine for simulation, but 1600 pins exceed any FPGA’s IO), so keccak_top streams the 25 lanes in and out over a 64-bit bus addressed by a 5-bit lane index. we writes din to lane idx; go launches the permutation; done marks completion; dout reads lane idx of the result. ~140 IOs — routes on the ECP5.

emit_ntt_butterfly_pipelined_verilog

Emit module name: emit_ntt_butterfly_verilog’s butterfly as a pipeline taking one butterfly a cycle, its result NttCuts::latency edges after its operands, registered after the steps cuts names. Each value a later stage reads reaches it through one register a stage, and only those values are carried.

emit_ntt_butterfly_verilog

Emit the combinational Montgomery fqmul + one Cooley–Tukey butterfly: inputs a, b (the two coefficients) and zeta; outputs hi = a + t, lo = a - t where t = fqmul(zeta, b) — all wrapping 16-bit, matching ntt_scalar’s inner step.

fqmul

montgomery_reduce

The reference Montgomery reduction (mirrors ntt::montgomery_reduce) — the oracle the emitted RTL is checked against.