# ML-KEM 多项式运算模块技术说明 ## 1. 运算域与数据表示 多项式运算位于环 `Z_q[x]/(x^256+1)`，其中 q=3329。系数在硬件中使用 12 位无符号模 q 表示。该组模块包括前向/逆向 NTT、Barrett 模乘、NTT 域 basecase 乘法、多项式加减以及 Compress/Decompress。算子使用 valid/ready 或 start/done 接口，由 `mlkem_top` 分时复用。 本文件中的 NTT、模乘、basecase、多项式加减、压缩模块及其局部 BRAM 均工作在 `mlkem_clk/mlkem_resetn`。算子与 `mlkem_top` 之间是单时钟域同步接口，不包含独立 CDC。 地址、valid 和数据的延迟对齐属于流水线时序问题，而不是跨时钟域问题。 ## 2. NTT 核 `ntt_core` 实现 256 点前向和逆向 NTT。系数存储由 `coeff_bram_4way` 划分为四个 Bank， 每个 Bank 具有同步读和写端口。地址生成器把同周期的两个蝶形对映射到互不冲突的 Bank， 从而同时处理四个系数。 数据通路包含两个 `butterfly_unit_pipe`。第 t 周期发出 BRAM 地址，下一周期取得系数， 随后进入流水化蝶形和 Barrett 模乘；写地址通过同长度延迟链与结果对齐。每层发射结束后 等待流水排空，再更新层号和旋转因子索引。逆 NTT 在七层变换后复用模乘流水线执行末尾 缩放。 `zeta_rom` 保存 128 个 12 位旋转因子。前向和逆向变换使用不同的索引方向及蝶形公式。 验证不能只比较 NTT 后的频域值，还应执行 INTT(NTT(a)) 并检查恢复系数，覆盖 Bank 地址 冲突和最后一层流水排空。 ## 3. Barrett 模约简与蝶形 `barrett_mul_pipe` 先计算 12x12 位乘积，再用常数 5039 估计除以 q 的商，计算 `r = p - q_est*q`，最后通过条件减 q 把结果限制到 `[0,q)`。各乘法级之间加入寄存器， 并以 `use_dsp="no"` 约束映射到 LUT。蝶形单元在模乘前后执行模加或模减，并将 valid 沿流水线传递。 商估计只在限定输入范围内成立，因此上游必须保证输入系数已经规范化。叶子测试应覆盖 0、q-1、乘积最大值和所有修正分支，不能仅使用随机中间值。 ## 4. NTT 域多项式乘法 `poly_mul_sync` 对 256 个频域系数按相邻偶/奇系数组成 128 个 basecase。每个 basecase 结合对应 zeta 计算两个输出系数。输入多项式写入独立 Bank，控制器按 LOAD、RUN 和 OUTPUT 阶段管理装载、流水计算和结果输出。 `basecase_mul_pipe` 并行计算多个模乘项，再完成模加。当前版本将系数存储改为偶/奇 Banked BRAM，减少离散寄存器和 LUTRAM。受同步 BRAM 读延迟和发射控制影响，RUN 阶段 每两周期发射一个 basecase。输出采用 valid/ready，接收端反压时不得覆盖尚未消费的系数。 `poly_arith_sync` 提供系数级模加和模减，用于点乘累加、噪声相加以及解封装中的差值。 运算结果在每一步规范化到模 q 范围，避免后续模乘输入超界。 ## 5. 压缩与解压缩 `comp_decomp_sync` 实现 FIPS 203 的 Compress_d 和 Decompress_d。压缩近似计算 `round(2^d*x/q) mod 2^d`，解压计算 `round(q*y/2^d)`。当前流水线使用常数乘法和移位 近似除法，避免综合组合除法器；模式、d 和 valid 随数据经过各级寄存。 输出端具有保持寄存器。当下游未 ready 时，结果和 valid 保持；输入 ready 由流水线及 输出可用性共同决定，因此文档和测试不应假设任意反压下始终每周期接收一个系数。需要 分别覆盖 d=1、4、5、10、11 等算法实际参数，并与精确整数公式逐值比较。 ## 6. 存储和调度约束 NTT 核和多项式乘法器各自包含局部 BRAM，ML-KEM 顶层还包含全局系数 Bank。进入算子前 需要将目标多项式装入局部存储，完成后再流式写回全局 Bank。这种结构简化端口仲裁，但 增加装载和回写周期。主 FSM 保证同一全局 Bank 端口在一个状态内只有一个所有者。 ## 7. 验证边界 叶子级验证应覆盖 NTT、INTT、basecase、完整多项式乘法、模加减和压缩解压，并对所有 256 个系数比较。顶层 KAT 能验证算子组合后的算法结果，但当多个误差互相抵消时不能定位 根因。实现后还需检查 BRAM 推断、DSP=0 和 valid/地址延迟对齐；这些属于结构验证，不能 仅由软件结果正确推出。