# xsim_run.tcl - Vivado XSIM for mlkem_top ML-KEM KeyGen, all K in {2,3,4}.
#
# Compiles the full KeyGen datapath + leaf modules, then runs the parametric
# NIST KAT testbench for ML-KEM-512 (K=2), 768 (K=3), 1024 (K=4). Each case
# verifies ek==KAT.pk and dk==KAT.sk byte-exact.
#
#   ./run_tb.sh top

# ---- Step 1: compile RTL ----
xvlog -sv --relax -i . sync_rtl/sha3/keccak_round.v
xvlog -sv --relax -i . sync_rtl/sha3/keccak_core.v
xvlog -sv --relax -i . sync_rtl/sha3/sha3_top_shared.v
xvlog -sv --relax -i . sync_rtl/sample_ntt/sample_ntt_sync_shared.v
xvlog -sv --relax -i . sync_rtl/sample_cbd/sample_cbd_sync_shared.v
xvlog -sv --relax -i . sync_rtl/ntt/barrett_mul.v
xvlog -sv --relax -i . sync_rtl/ntt/zeta_rom.v
xvlog -sv --relax -i . sync_rtl/ntt/butterfly_unit.v
xvlog -sv --relax -i . sync_rtl/ntt/ntt_core.v
xvlog -sv --relax -i . sync_rtl/poly_mul/basecase_mul.v
xvlog -sv --relax -i . sync_rtl/poly_mul/basecase_mul_pipe.v
xvlog -sv --relax -i . sync_rtl/poly_mul/poly_mul_zeta_rom.v
xvlog -sv --relax -i . sync_rtl/poly_mul/poly_mul_sync.v
xvlog -sv --relax -i . sync_rtl/storage/sd_bram.v
xvlog -sv --relax -i . sync_rtl/common/pipeline_reg.v
xvlog -sv --relax -i . sync_rtl/comp_decomp/comp_decomp_sync.v
xvlog -sv --relax -i . sync_rtl/top/mlkem_top.v

# ---- Step 2: compile parametric KAT testbench ----
xvlog -sv --relax sync_rtl/top/TB/tb_mlkem_kg_katK_xsim.v

# ---- Step 3: elaborate one snapshot per K ----
xelab tb_mlkem_kg_katK_xsim -generic_top KP=2 -s mlkem_kg_k2 --timescale 1ns/1ps
xelab tb_mlkem_kg_katK_xsim -generic_top KP=3 -s mlkem_kg_k3 --timescale 1ns/1ps
xelab tb_mlkem_kg_katK_xsim -generic_top KP=4 -s mlkem_kg_k4 --timescale 1ns/1ps

# ---- Step 4: run KAT cases (K=2: 0..4, K=3/4: 0..2) ----
xsim mlkem_kg_k2 -R -testplusarg CASE=0
xsim mlkem_kg_k2 -R -testplusarg CASE=1
xsim mlkem_kg_k2 -R -testplusarg CASE=2
xsim mlkem_kg_k2 -R -testplusarg CASE=3
xsim mlkem_kg_k2 -R -testplusarg CASE=4
xsim mlkem_kg_k3 -R -testplusarg CASE=0
xsim mlkem_kg_k3 -R -testplusarg CASE=1
xsim mlkem_kg_k3 -R -testplusarg CASE=2
xsim mlkem_kg_k4 -R -testplusarg CASE=0
xsim mlkem_kg_k4 -R -testplusarg CASE=1
xsim mlkem_kg_k4 -R -testplusarg CASE=2