K-PKE.Decrypt step 1 (FIPS 203 Alg 15): decode+decompress the ciphertext.
- comp_decomp_sync instance made mode-selectable: Encaps C1/C2 still compress
(mode 0), Decaps ST_DEC_DECOMP decompresses (mode 1) with d=du/dv.
- New ST_DEC_DECOMP state with an inline byteDecode_d walker (reverse of the
C1/C2 bit-packer): walks c_in_bram bytes, accumulates LSB-first into a bit
buffer, extracts d-bit symbols, feeds comp_decomp, writes each decompressed
coeff (mod q) to a bank.
c1 = K polys, d=du -> u'[i] in bank_se rel slot i (0..K-1)
c2 = 1 poly, d=dv -> v' in bank_t rel slot DEC_VSLOT=2 (avoids UPSUM=1)
- dbg_slot_i widened 4->6 bits so the TB can read v' (abs slot 26 at K=4).
- bse/bt write muxes gain the DECOMP writeback paths (dec_u_we / dec_v_we).
Verification: examples/dump_decaps.rs (ml-kem-r worktree) emits per-stage
golden (u'/v'/s_hat/u_hat/w/m') into vectors/decgold/. TB verify_d1 reads back
u'[i] and v' and compares all 256 coeffs each.
Bring-up note: dbg coeff readback latency is bank(1)+dbg_coeff_r(1); the TB's
rdcoeff initially waited 2 cyc and saw data shifted by one index -> fixed to 3.
Verified: dec D1 K=2/3/4 all cases PASS; KeyGen + Encaps unregressed.
Verilator is no longer used (all verification is via Vivado XSIM). Remove:
- 10 per-module tb_*.cpp Verilator testbenches
- the entire test_framework/ Verilator harness (lib/, run_all.py, config.json,
per-module test_plan.json/gen_vectors.py, golden vectors, reports)
- stale specs: verilator-conventions.md, test_framework/structure.md
(index.md updated to drop the Verilator entry)
Parallelize run_tb.sh K x case execution (modules stay serial):
- new run_xsim_jobs helper: compile+elaborate once (serial, populates the
shared xsim.dir), then run each (K,case) xsim in its own private workdir
with a COPY of xsim.dir (~1MB) so concurrent same-snapshot runs don't clobber
each other's runtime logs. Each workdir symlinks the repo sync_rtl tree so
the TB's repo-relative $readmemh vector paths resolve.
- top/enc/dec runners refactored to build a (snapshot:K:case) spec list and
hand it to run_xsim_jobs; ordered PASS/FAIL summary + per-job /tmp logs
preserved. Bare './run_tb.sh top' now also takes the parallel path.
Speedup (20 cores): top full sweep 2:11 -> 0:51 (~2.6x), ~320% CPU.
Verified: top (11) / enc (9) / dec (9) all PASS; missing-vector runs still
fail (file-not-found guard -> exit 1).
Scaffolding for ML-KEM Decaps (FIPS 203 Alg 18):
- op_i widened to 2-bit: 00=KeyGen, 01=Encaps, 10=Decaps (op_r too).
- New ST_DEC_LOAD state (D0: settles to DONE so load/parse is dbg-checkable).
- dk (=sk) streamed via dk_in_*; load logic routes each byte by region:
[0,384K)->dk_pke (dkp_bram), [384K,768K+32)->ek_pke (ek_bram),
[768K+32,+32)->H(ek) (hek_r), [768K+64,+32)->z (z_r). Routing uses the
LIVE k_i input, not start-captured k_r (dk is streamed before start_i).
- c (=ct) streamed via c_in_* into a SEPARATE c_in_bram, so the computed c'
(ct_bram) can later be compared against original c and J(z||c) can read c.
- New dbg taps: dbg_mprime_o/dbg_kbar_o/dbg_decz_o/dbg_dech_o.
TB: tb_mlkem_dec_katK_xsim verifies dk parse (H(ek), z, ek_pke/dk_pke BRAM
round-trip). gen_decaps_vectors.py emits dec_k{K}_c{N}_{dk,ct,ss,ctn,ssn}.hex
from the NIST KAT. run_tb.sh gains a 'dec' module (mirrors 'enc').
Regression fix: old KeyGen/Encaps TBs didn't connect the new input ports,
floating them to X and corrupting the ek/dkp write muxes -> tied off
dk_in_*/c_in_*/new dbg taps in both.
Verified: dec D0 K=2/3/4 PASS; KeyGen K=2 + Encaps K=2 unregressed.
run_tb.sh gains an 'enc' module that shares the 'top' KeyGen tcl compile
list (same RTL datapath) and swaps in tb_mlkem_enc_katK_xsim. Usage mirrors
'top': ./run_tb.sh enc [K] [CASE]; no args -> full sweep K=2/3/4 cases 0..2.
--list shows enc; per-case summary lines parse PASS (E7). run_enc.sh deleted.
tb_mlkem_enc_katK_xsim verify_e7 now dumps the hardware-produced ct (read
from ct_bram via the dbg_ct tap) on one line (byte 0 first), same format as
ml-kem-r's encaps_io example, so ss/ct can be eyeballed and diffed. On
mismatch it re-scans to print the first 8 differing byte positions.
Verified: ./run_tb.sh enc -> 9/9 PASS (E7) (ct==KAT.ct && ss==KAT.ss);
./run_tb.sh top 3 0 KeyGen unregressed.
Reuses the E5 bit-packer FSM for ST_ENC_C2, generalized over region:
- coeff source: cp_coeff_src = bank_t[UPSUM] (v) for C2, bank_se (u) for C1
- bit width: cp_d already = dv_rt for C2 else du_rt
- poly count: cp_poly_max = 1 (single v) for C2, K for C1
- ct write pointer cp_wa CONTINUES from c1_bytes into C2 (not reset), so c2
lands right after c1. c1 ends on a whole-byte/poly boundary (256*du/8
integral), so cp_buf/nbits are empty at the C1->C2 handoff.
FSM tail: ST_ENC_V -> ST_ENC_C2 -> ST_DONE.
TB: verify_e7 compares the full ct (c1||c2, CTB bytes) to KAT.ct byte-exact
via the dbg_ct tap. Combined with the E0 ss==KAT.ss check this is the full
end-to-end Encaps KAT (ct==KAT.ct && ss==KAT.ss).
Verified end-to-end for K=2/3/4, cases 0-2 (K2) / 0-1 (K3,K4):
ct==KAT.ct && ss==KAT.ss. ML-KEM Encaps complete. KeyGen unregressed.
Storage choreography (per plan risk notes):
- TDEC now decodes t_hat[j] into bank_a slot j*K (was bank_t). This makes
V's MAC reuse E4's u_aslot=u_j*K+u_row addressing with u_row=0, no mux
change. bank_t has no room for K=4 (t_hat would fill all 4 slots vs
psum's UPSUM slot), hence bank_a (16 slots, A_hat dead after E4).
- New ST_ENC_E2MV state relocates e2 (bank_t[0]) -> bank_a[1] so V-ADD
reads psum (bank_t) and e2 (bank_a) from different banks (no port
conflict). bank_se (y_hat + u) stays intact -> verify_e2/e3/e4 unaffected.
- V reuses the u_* MAC/INTT/ADD machine with u_row tied to 0 (u_row_max=1).
ADD computes psum + e2 + mu mod Q -> bank_t[UPSUM] in place;
mu[w] = m_r[w] ? 1665 : 0 (Decompress_1). FSM: C1->TDEC->E2MV->V->DONE.
Bug found+fixed during bring-up: e2 relocation was off-by-one (wrote
e2[i+1] into slot i) because em_we/em_widx were registered an extra cycle
past the bram read. Fixed: em_widx==em_ridx, write scheduled for the cycle
bt_rd_data presents e2[em_ridx].
TB: verify_e6 compares v (bank_t dbg slot 9, K=2) to ml-kem-r golden.
verify_e1 dropped (TDEC overwrites bank_a A_hat slots; A_hat transitively
verified by E4). Verified: K=2 E2/E3/E4/E6 == golden, E5 c1 == KAT prefix;
K=3/4 E0+E5 pass; KeyGen K=2 unregressed.
ST_ENC_C1: per-coeff Compress_du via comp_decomp_sync (mode 0) then
LSB-first byte packing into ct_bram. 5-phase micro-seq reads u[cp_poly]
from bank_se (rel K+poly), feeds the compressor (1-cyc pipe), appends du
bits to cp_buf, and drains whole bytes. Each poly = 256*du bits (whole
bytes) so the bit buffer empties at every poly boundary.
ST_ENC_U now advances to ST_ENC_C1 (was ST_DONE).
TB: verify_e5 compares ct_bram[0..c1_bytes-1] to the KAT.ct prefix via
the dbg_ct tap. run_enc.sh: encaps TB runner (compiles comp_decomp_sync
which the KeyGen tcl omits).
Verified K=2/3/4 c1 == KAT.ct prefix (640/960/1408 B; K=4 du=11
cross-byte path), K=2 cases 0-2.
Extend mlkem_top with a runtime op_i select (0=KeyGen, 1=Encaps) and the
first Encaps stages, reusing the shared keccak_core and the ST_H multi-block
SHA3-256 machinery:
ST_ENC_H: H(ek) over preloaded ek_bram (same FSM as KeyGen ST_H)
ST_ENC_G: (K,r) = G(m||H(ek)) via new 64-byte single-block SHA3-512
- sha3_top_shared: add mode=2'b11 = SHA3-512 over a full 512-bit message
(g512_pad). Standalone tb_sha3_g512 confirms it byte-exact.
- mlkem_top: new ports op_i, msg_i, ek_in_{we,addr,byte} (ek preload), ss_o,
dbg_ct_*, dbg_r_o/dbg_hek_o. st widened 4->5 bits; ST_ENC_* states added.
Renamed message port to msg_i to avoid collision with ST_M counter m_i.
- TB tb_mlkem_enc_katK + gen_encaps_vectors.py (per-byte ek/m/ct/ss vectors).
Verified ss==KAT.ss for K=2/3/4, cases 0-2 (all PASS). KeyGen unaffected
(K=2 c0 still ek==pk, dk==sk byte-exact).
Replace the single async-read polymem[0:28*256-1] with 3 polynomial-indexed
banks (bank_a A_hat / bank_se s_hat||e_hat / bank_t t_hat), addressed by
abs_slot - base_slot. Still async-read here -- a pure refactor that validates
bank sizing and base-relative addressing with zero timing change before
stage 2b converts them to registered sd_bram + read-ahead pipelines.
11/11 KAT PASS, byte-exact, 0 file-not-found.
