计算机体系结构 E01：从教学模型到 RTL

核心问题

把 Python 教学模型改写成 SystemVerilog，什么时候才算得到了一份可验证的 RTL？语言文件存在只证明描述已经写下；功能仿真、综合、静态时序分析和 FPGA 上板分别回答不同问题，不能互相代替。

附件：E01-rtl.json、rv32i_core.sv和testbench.sv。

范围与证据等级

随文两次加法状态机的功能证据来自旧 Linux 批次的 Icarus Verilog 12 仿真及逐提交差分。2026-10-01 本地同时保留这份源码和 examples/computer-architecture/rtl/src/ 下的累计 RTL、四程序输入及历史差分；本轮未安装 Icarus，未重新仿真。两套源码与记录分别使用，历史记录不能替另一份源码验收。

随文 RTL 进一步缩成三状态行为：复位后令 x1=0，随后执行两次 addi 等价更新，最终 x1=12 并 halt。它只用于说明时钟边沿上的状态更新，不是完整 RV32I 核。

核心案例：仿真通过没有跨过物理实现边界

testbench 产生时钟、释放 reset、等待 halt，并断言 x1 必须为 12。这个检查能发现状态转移错误，却没有综合出门级网表，也没有 Liberty 工艺库、STA 约束、布局布线或板卡信号。

riscv-formal 还需要 RVFI 等接口和形式工具链。当前 RTL 没有接入这些接口，因此不能用普通 testbench 的 PASS 替代形式验证或 ISA 合规结论。

模式：每种工具只签一层结论

仿真 → 功能轨迹
综合 → 逻辑映射
STA → 约束下的时序
上板 → 目标器件行为

RTL、协议状态机和硬件加速器模块都应按这四层保存证据。上一层通过不会自动签署下一层。

验收结果

旧 Linux 批次用 Icarus 12 对两次 addi 状态机仿真：参考执行器与 RTL 均提交 (pc=0,x1=7)、(pc=4,x1=12)；把第二次加数改成 6 后，测试台以状态 1 退出且第二条提交分歧。2026-10-01 本地运行 python3 examples/computer-architecture/run_batch.py E01-E08 因缺少 Icarus 非零退出，明确记录 executed_now=false。

累计核心另由 examples/computer-architecture/rtl/scripts/run_all.sh 管理四程序差分，需指定可执行的 IVERILOG 和 VVP 后复跑。源码、输入与历史输出均已存在，不再属于同步缺失；综合、STA、FPGA、riscv-formal 仍未运行。

模式速查

证据	支持	不支持
testbench 功能仿真	给定输入的 RTL 状态轨迹	综合与时序收敛
综合网表	逻辑可映射	板上功能正确
RVFI 形式检查	声明性质与范围	未声明的完整实现行为