update system design report

doc/reports/system/modules/09_mlkem_polynomial_arithmetic.md

@@ -0,0 +1,72 @@
+# 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/地址延迟对齐；这些属于结构验证，不能
+仅由软件结果正确推出。