计算机体系结构 E08：有限模型与形式验证边界
计算机体系结构 E08：有限模型与形式验证边界
核心问题
穷举数万个程序都没找到反例，是否等于处理器对任意程序都正确？只有状态空间、初态、程序长度和性质全部明确时，“无反例”才有意义；有限穷举不能自动升级成无界证明或 ISA 合规认证。
附件：E08-formal.json和检查器源码。
范围与证据等级
证据等级为功能执行。模型固定 4 个寄存器、8 个 memory word、初始寄存器 (0,1,2,4) 和全零内存；text 区为 word index [0,4)。指令集合共有 208 个具体变体，程序长度只取 0、1、2。
检查的两个性质是 x0 恒为 0，以及 store 不修改 text 区。sw 地址在模型里是 word index，不是 RISC-V 字节地址。异常、中断、页表、并发和更长程序均未覆盖。
核心案例：43,473 来自完整计数，不是估计
长度 0 有 1 个空程序，长度 1 有 208 个程序，长度 2 有 208²=43,264 个程序，总数为 43,473。检查器逐个执行并断言两个性质。
错误变体允许写 x0，长度 1 的 addi x0,x0,-1 立即给出反例，x0 变成 0xffffffff。反例说明性质检查能捕获这一类故障，但不证明检查器没有共同建模错误。
模式：结论强度不得超过量词范围
1 | |
差分测试、有界模型检查和协议状态搜索都应把量词写进结论。要得到无界性质，还需要归纳不变量、定理证明或覆盖更强的形式框架。
验收结果
python3 examples/computer-architecture/run_batch.py E01-E08 退出 0，完整遍历 43,473 个程序，两个性质均通过；错误 x0 变体产生一条长度 1 的反例。输出保留 unbounded_proof=false。
模式速查
| 方法 | 当前覆盖 | 不能替代 |
|---|---|---|
| 有限穷举 | 声明空间内全部程序 | 无界证明 |
| 故障注入 | 检查器可发现该 bug | 检查器完备性 |
| 差分测试 | 两个模型在样本上一致 | 两者都符合 ISA |
一手参考资料
All articles on this blog are licensed under CC BY-NC-SA 4.0 unless otherwise stated.
Related Articles
2026-09-19
计算机体系结构 15：仿真结果怎样可信
仿真结果怎样可信 一个模型输出“程序结果为 25，耗时 100 周期”，包含两类不同的断言。结果为 25 需要检查指令语义；100 周期需要检查阶段、端口、队列和延迟假设。即使两者都符合模型定义，仍不能直接推出某台真实处理器也会耗时 100 周期。 本篇的核心问题是：怎样把功能正确、模型内部一致和硬件拟合分开验收？已执行的核心案例是同一批 RV32I 程序的独立解释器差分，并通过故意破坏 x0 规则验证检查器确实能发现错误。统计口径另用第 13 篇事件记录手算。gem5 部分提供指定版本的待运行配置，状态为 NOT_RUN，没有本系列的 gem5 仿真结果。 实验目录为 examples/computer-architecture/ooo/。可下载 差分结果、统计口径记录、运行环境 和 Python 功能解释器。这些文件对应功能执行或手算证据，不是硬件测量。 三个验证问题分别需要什么证据 功能验证关心给定输入是否产生规定的架构状态变化。对第 07 篇的有限执行器，可以逐条比较 PC、目标寄存器和值、内存地址和值、分支方向，以及正常结束或拒绝原因。 时序验证关心程序在声明的资源和事...
2026-09-29
计算机体系结构 E06：可靠性与持久性
计算机体系结构 E06：可靠性与持久性 核心问题 CPU 已经读到新值，是否意味着掉电后还能读到它？可见性只描述运行中的读取关系。持久性还要区分写回已经发起、仍在 pending、已经 drained，以及持久域是否能在掉电时保存对应数据。 附件：E06-reliability.json。 范围与证据等级 证据等级为功能执行。第一部分穷举固定 extended Hamming (8,4) 教学码；第二部分执行五个持久状态，但不连接真实 NVDIMM、filesystem 或 PMDK。模型不能代表 ECC DIMM、Chipkill 或任意长度事务原子性。 核心案例一：纠错能力必须写出码字范围 布局使用 4 个数据位、3 个 Hamming parity 位和 1 个 overall parity 位。16 个数据字的无错编码全部判为 clean；每个 8 位码字的 8 个单比特翻转共 128 个，全部归类为可纠正；每个码字的 28 个双比特组合共 448 个，全部检测为双错。 这组穷举只覆盖固定码。双错“检测到”不等于“纠正”，更多比特同时翻转也没有保证。 核心案例二：visi...
2026-09-19
计算机体系结构 08：多周期执行
多周期执行：怎样在几拍之间保存一条指令 一条 lw 要取指、读基址、计算地址、读取内存，最后写回寄存器。若这些动作必须在一拍里结束，时钟周期就要覆盖整条路径。把它拆成几拍可以缩短每拍必须完成的组合路径，也允许同一硬件部件在不同拍承担不同任务。代价是指令要占用更多周期，控制器还必须保存中间结果。 中心问题是：拆开的每一拍究竟保存什么，下一拍怎样知道继续做哪一步？本篇用第 07 篇相同的 .hex 求和程序，构建实际推进状态的多周期解释器。证据等级包括“教学时序模型”和带明确题设的“手算”。模型没有门级网表、综合时钟或面积数据，因此不能据此断言某块硬件变快或变小。 保存状态以后，组合逻辑才能跨拍复用 单周期通路中的某个中间值在该拍内一直可见。进入多周期设计后，组合逻辑输入可能在下一拍改变；后续仍要使用的值必须写进寄存器。指令字需要 IR，寄存器堆的读出值需要 A/B，地址或算术结果需要 ALUOut，读取内存的结果需要 MDR。实际实现可以合并或重新命名这些寄存器，所保存的信息不能凭空消失。 Berkeley CS152 的多周期数据通路讲义展示了这些跨周期寄存器及控制状态。讲义使用...
2026-09-29
计算机体系结构 33：性能、功耗与能量预算
计算机体系结构 33：性能、功耗与能量预算 核心问题 平均功率下降，为什么完成同一任务的能量仍可能上升？功率描述单位时间的能量变化，任务能量还要乘以持续时间。降频降压可能降低动态功率，却也会拉长执行时间；静态功耗、内存和其他系统部件在延长的时间里仍在消耗能量。 本篇只做两个题设点的能量预算。附件：33-energy.json。 范围与证据等级 证据等级为手算。当前没有采集 RAPL、Linux powercap、板级功率计、频率、温度或硬件计数器。题设中的 40 W、25 W、2 s 和 4 s 都是模型输入，不对应当前宿主的传感器读数。 能量关系为： 1energy(J) = average power(W) × elapsed time(s) 动态 CMOS 功耗常用 αCV²f 解释电压、频率和活动因子的关系，但真实芯片还包含泄漏、供电转换、内存与散热等成本。没有测量就不能把公式写成某颗 CPU 的能耗结论。 核心案例：低功率点消耗更多任务能量 快点题设为 40 W、2 s，任务能量是 80 J。慢点功率降到 25 W，但运行 4 s，任务能量变为 100 J。功率下降 3...
2026-09-05
从零编写现代编译器 21 - 差分、属性与模糊测试
手工测试用例覆盖的是写测试的人想得到的错误。想不到的错误藏在组合空间的角落里，等着在生产环境被触发。前面二十篇积累了解释器、编译器、优化 pass 和源码映射，手工正反例加起来几百条，仍然不能保证它们之间没有分歧。 本篇用随机生成的 Sprout 程序同时喂给解释器和编译后的本机二进制，比较两边的输出。任何不一致都意味着 bug。找到之后自动缩减失败样本，留下最小复现，纳入回归语料。 差分测试：两条路径，一个判定 差分测试的核心逻辑只有一句话：同一个程序经过两条独立的执行路径，结果必须一致。 123456789随机生成合法 Sprout 程序 P │ ├─ 解释器（第 07 篇）执行 P → 退出值 A, stdout A, 错误类别 A │ └─ 编译器 → 本机二进制 → 执行 → 退出值 B, stdout B, 错误类别 B │ 比较 (A, B) 一致 → 通过 不一致 → 记录 P，进入缩减流程 比较的不是错误消息的字面文本。解释器报 division by zero at line 5，编译后的运行时报 runtime error: div...
2026-09-29
计算机体系结构 29：CPU 怎样与设备交换数据
计算机体系结构 29：CPU 怎样与设备交换数据 核心问题 设备完成一次 DMA 后，CPU 为什么还不能立刻把缓冲区当成普通内存读取？数据移动只是传输链路的一部分。驱动还要处理 DMA 地址映射、缓冲区所有权、完成通知和同步；IOMMU 则可能在设备地址与物理内存之间再加一层翻译和权限检查。 本篇只验证一条六状态协议，不连接真实设备，不产生总线事务，也不测中断延迟。附件：29-dma.json。 范围与证据等级 证据等级为功能执行。模型依次进入 cpu_owned、mapped_for_device、device_owned、completion_visible、synced_for_cpu、cpu_consumed。这些状态用于检查“谁此时可以访问缓冲区”，不能证明某个平台的 DMA 一致性实现，更不能称作真实设备传输。 Linux Dynamic DMA Mapping Guide 区分 CPU 虚拟地址、CPU 物理地址和设备使用的 DMA 地址。驱动应使用 DMA API 建立映射，不能把 CPU 指针直接交给设备。streaming mapping 的同步要求还取决于...