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

核心问题

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

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

范围与证据等级

证据等级为功能执行，来源是 2026-09-22 保存的 Icarus Verilog 13.0 仿真记录；当时四个程序的逐提交差分通过，并检出了 x0 写回故障和截断轨迹。当前容器没有 iverilog 或 vvp，本轮没有复跑这些结果。

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

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

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

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

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

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

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

验收结果

python3 examples/computer-architecture/run_batch.py E01-E08 记录 executed_now=false，并明确保存 synthesis、STA、FPGA、riscv-formal 均为 false。历史功能仿真可追溯，当前未复跑的缺口保留。

模式速查

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

一手参考资料

• Icarus Verilog：Getting Started
• Verilator：Input Languages
• YosysHQ：riscv-formal