The old script referenced 5 non-existent files (keccak_arbiter,
sha3_chain_top_shared, tb_mlkem_top_xsim, tb_kg/en/de) and stale
vectors, so read_verilog/elaborate failed outright.
Rewrite to mirror the verified XSIM flow (sync_rtl/top/TB/xsim_run.tcl):
- load exactly the 14 sources mlkem_top depends on
- sim top = tb_mlkem_kg_katK_xsim, runtime K via generic KP, case via
-testplusarg CASE
- copy KAT vectors into the xsim working dir via xsim.compile.tcl.pre
(the only hook in 2019.2 that runs before $readmemh; an appended
-tclbatch runs after Vivado's own 'run all', too late)
- drop duplicate --relax (XSim adds it; passing again is an error)
Verified through the actual Vivado batch project flow:
K=2 CASE 0 -> PASS (21403 cyc), K=4 CASE 2 -> PASS (54059 cyc),
0 file-not-found warnings. gitignore the generated vivado_prj/.
Also rewrite README.md in Chinese documenting the mlkem_top workflow
and test flow.
Adds 4 Verilator cases covering d_u=11 and d_v=5 (ML-KEM-1024), which the
RTL already supports (d is 5-bit, products fit 24 bits). comp_decomp now
120/120 vectors. Also ignore .omo/ session runtime cache and archive the
06-27-sha3-g-test-specific-input trellis task.
Verified all 10 modules pass both frameworks:
- Verilator: 4334/4334 vectors
- XSIM (Vivado 2019.2): all 11 testbenches green, separate committed vectors
Oracles independently cross-checked vs hashlib (G/H/J/PRF) and FIPS 203
Alg 7/8/9/10/12 (sample_ntt, sample_cbd, ntt, poly_mul).
sample_ntt was non-conformant: both RTL and the test reference re-ran
keccak_p after every 3-byte squeeze instead of consuming the full
1344-bit SHAKE-128 rate. Only coeff[0] matched a standard sampler, so
the generated A matrix would not interoperate with any compliant ML-KEM.
- sample_ntt_sync{,_shared}.v: walk all 56 groups of the rate block via
grp_ptr_r; re-permute only when the block is exhausted. Verified
256/256 against ml-kem-r Rust sample_ntt on two seeds, and 1536/1536
in the Verilator framework (runtime ~128x faster per poly).
- gen_vectors.py: use a self-contained hashlib.shake_128 oracle.
sha3 testbench fixes (all now self-check hash_o against verified vectors,
cross-checked with hashlib and ml-kem-r mlkem_G):
- tb_sha3_xsim_simple.v: test G/H/J modes, not just G.
- tb_keccak_core_xsim.v: correct the wrong EXPECTED_STATE constant
(RTL was correct; lane0 = 0xf1258f7940e1dde7 per FIPS 202).
- tb_sha3_xsim.v: read expected file and self-check per vector; add
vectors/g_basic_{input,expected}.hex (3 G / 2 H / 2 J).
Remove stale sha3_chain test (its RTL was deleted in 1cace51) and its
README references. Extend .gitignore for XSIM artifacts and result dumps.
