VAMP — 把一颗有流水线、乱序、浮点和 cache 的处理器从门电路证到指令集

是什么

VAMP（Verified Architecture Microprocessor）是 Verisoft 项目里那颗被一证到底的 RISC 处理器。和它的母项目 verisoft-2008 不同，本论文聚焦在硬件这一层：把一颗有 5 段流水线、Tomasulo 乱序、IEEE-754 浮点、MMU、cache 一致性的真处理器，在 Isabelle/HOL 里从门电路一路证到指令集语义。

日常类比：发动机厂家不光说「我这台 V8 输出 400 马力」，他们还把每一根活塞、每一个气门、每一颗螺丝在显微镜下拍下来，证明这堆零件组装起来就是 400 马力 —— 而且证明用的是数学，不是路试。

为什么重要

在 verisoft-2008 那篇综述里 VAMP 只占一小段，因为它的工程量在那篇里被压缩了。但 VAMP 本身是 6 个人 4 年的活，单独一篇 30 页论文。不理解 VAMP，下面这些事都讲不清。

为什么 sel4 不证 CPU —— Verisoft 已经做过一次，知道代价多大
为什么 RISC-V 形式化（Sail-RISC-V）从 ISA 出发不是门电路 —— VAMP 给出了门电路证明的真实成本
浮点证明是其中最难的部分，IEEE-754 几百页规范要全部翻进 Isabelle —— 工程量后来被 HOL Light 证 Kepler 猜想的同代工具继承
Tomasulo 乱序证明是早期少数几个完整证完的乱序处理器证明之一（同期还有 Sawada-Hunt 在 ACL2 里的工作），方法学被工业级 CPU 验证（如 Centaur 的 ACL2 证明）借鉴

核心要点

VAMP 的证明结构可以拆成 5 件事。

RTL 层 vs ISA 层 —— 两套语义之间架桥：RTL（register-transfer level）层用 Isabelle 把每个寄存器、ALU、控制信号都写成布尔函数；ISA 层是抽象的「执行 ADDI 加一个立即数」。证明定理：若 RTL 跑 N 个时钟周期，则 ISA 跑了 K 条指令（K ≤ N，因为流水线有 stall 和 mispredict）。
Tomasulo 乱序 —— 调度器 + 重排序缓冲：Tomasulo 是 1967 年 IBM 提出的指令调度算法，让多条指令同时跑在不同执行单元上，但最后还是按程序原始顺序「提交」结果。VAMP 实现了 Tomasulo 算法（保留站、CDB 公共数据总线、ROB 重排序缓冲）。证明的核心是「虽然指令乱序执行，但提交顺序和 commit 阶段写回的状态等价于顺序语义」。这比顺序流水线难一个数量级。
IEEE-754 浮点：完整支持 32/64 位浮点，4 种舍入模式（near/zero/+inf/-inf），denormal 数。证明 ALU 电路 = IEEE 算术抽象定义。这一块独立成两位博士的论文（Berg, Jacobi）。
MMU 和 cache：MMU 证明虚拟地址 load/store 等价于物理地址语义 + 页表查询；cache 证明对软件不可见 —— 程序看到的内存语义和「没有 cache」时一致。
和 C0 编译器 / VAMOS 内核的接合：VAMP 的 ISA 层正好是 C0 编译器证明的目标语义。两者用同一个 Isabelle 状态空间，所以「C0 程序在 VAMP 上跑」的端到端定理可以拼出来。

实践案例

案例 1：RTL 一个时钟周期到底证什么

Isabelle 里写 step_RTL : RTL_state → RTL_state，定义为「所有寄存器同时按当前控制信号更新」。要证明的是：

step_RTL 重复 N 次后的相关寄存器值
  ＝
step_ISA 重复 K 次后的值

难点在于 stall（流水线气泡）和 forwarding（旁路）—— 两者让 N 和 K 不再 1:1。证明里要构造一个「映射函数」从 RTL 状态抽出 ISA 状态，然后归纳证每一步都保持这个映射。

案例 2：浮点为什么难证

IEEE-754 加法的电路实现一共 4 步：先对齐指数（移位）、加尾数、规范化、舍入。每一步都可能溢出/下溢/产生 NaN。Isabelle 里要证：

电路输出 = round(real_add(a, b))

其中 round 按 4 种舍入模式之一。光是证明「移位电路移对了位数」就要几百行 Isar。整个浮点单元证明大概 5 万行。

案例 3：Tomasulo 乱序的精化关系

乱序证明的核心思想是找一个精化关系（refinement）：

乱序硬件的可观测行为（提交到寄存器的写、内存的写）
必须等价于某个顺序语义下指令一条一条执行的可观测行为

证明的关键不变量是「ROB 里所有指令按 program order 排队，commit 阶段必然按这个顺序写回」。投机执行的指令如果触发异常，在 commit 之前会被抛弃 —— 这一点写漏一行下面整套证明就崩。

案例 4：端到端流是怎么走通的

邮件客户端用 C0 写。两条 lemma 拼起来就是端到端定理：

C0 编译器证明给你「C0 程序 P 的语义 = 编译产物 P′ 在 VAMP-ISA 上的语义」
VAMP 证明给你「VAMP-ISA 的语义 = VAMP-RTL 上 N 个周期的行为」

Isabelle 里把这两条复合一下，就有了「C0 源代码 → 物理硬件」的总定理。这就是 verisoft-2008 那一句「端到端」的真正意思。

踩过的坑

投机执行 + 异常组合最坑：投机指令产生异常但还没提交时怎么处理，规约写错下面整套证明就崩。Jacobi 的博士论文有专门一章讲这件事。
浮点 denormal 的处理代价：很多商用 CPU 在 denormal 时会触发慢路径软件模拟。VAMP 选择全硬件实现，证明工作量翻倍 —— 但换来的是「硬件总能在固定时钟数内完成」这个性质。
Cache 一致性只证单核：多核 cache 一致性（MESI 协议等）在 VAMP 范围之外，是 Verisoft XT 后续话题。
证明只覆盖行为正确，不覆盖时序闭合（电路能不能跑到 1 GHz）。这是综合工具的事，证明工具不管。所以 VAMP 「证完」不等于「能流片」。
RTL 不是直接从 Verilog 翻译的，是 Isabelle 里手写的「等价 RTL」。工业 CPU 验证还要再加一层 Verilog → Isabelle 翻译，这一步在 VAMP 里没做。
改一行实现可能要重证几千行：流水线的 forwarding 路径加一条，整个步进定理的归纳要重做。这是为什么证明工程很难做迭代式开发。

适用 vs 不适用场景

适用：

教科书 —— 给学生看「流水线 + 乱序 + 浮点」完整证明长什么样
启发后续 —— RISC-V Sail 模型、ARM 机器可读 ISA 都从 VAMP 学到「先把 ISA 写成可执行规约」
安全 CPU 设计 —— 航天/医疗/密码硬件需要类似深度的证明
教学 —— Saarland 的体系结构课直接用 VAMP 当教具

不适用：

工业 x86 / ARM —— 体积太大，证明做不动；VAMP 是简化 DLX
多核 / NUMA —— VAMP 只有单核
动态频率 / 低功耗 —— 证明里没有时序细节
软核移植 —— RTL 是 Isabelle 写的，不能直接喂给综合工具

历史小故事（可跳过）

1992-1995：Wolfgang Paul 在 Saarland 教《计算机体系结构 II》，开始用 PVS 证 DLX 处理器（前身 DLX-PVS）。
2002：项目转到 Isabelle/HOL，方法学定稿。
2003：Verisoft 主项目启动，VAMP 成为硬件层主体。
2003-2005：Beyer 做流水线、Jacobi 做 Tomasulo、Berg 做浮点、Kröning 做 MMU、Leinenbach 做编译器接口 —— 5 个博士论文同时推进。
2006：本论文发表，把 5 个博士论文的方法和定理拼成一篇 30 页综述。
2007：VAMP 投到 FPGA 上真跑起来 —— 证完的硬件设计变成可综合 RTL。
2010 年后：方法学被 Verisoft XT 用到 x86 ISA 证明，但不再下到门电路那一层。

学到什么

证 CPU 的瓶颈是规约，不是证明：写出 ISA 的形式语义、IEEE-754 的形式语义、MMU 的形式语义比证明本身难。
乱序证明 = 精化关系：找到一个「序列化模型」和实际乱序执行之间的对应，剩下的就是按结构归纳。
浮点是严格的代数，不是「差不多的数字」 —— 证明对就是对，错就是错，没有中间态。
硬件证明给上层无忧的地基：C0 编译器证明里直接假设「硬件是对的」，省下大量边界讨论。
学术 vs 工业方法不同：学术性硬件验证（VAMP）强调端到端，工业性硬件验证（Centaur ACL2、Intel FV）强调局部深。两者都对，看目的。
证明工程不是学术副产品：要工具链、CI、回归 —— VAMP 项目结束后大部分工件没人维护，是这件事被低估的代价。

关联

verisoft-2008 —— VAMP 是这个项目的硬件层；端到端定理由两者拼出
isabelle-hol-2002 —— VAMP 的主证明工具，用 Isar 写出 5 万行浮点证明
compcert —— 同期、同领域、不同 ISA 的 C 编译器证明
cakeml —— 后辈，自举 ML 编译器，目标 ISA 用 Sail
hol-light-2009 —— 浮点证明同代工具，证 Kepler 猜想用同套技术
acl2-2000 —— 工业 CPU 验证的另一条路（Centaur 用 ACL2 证 x86 子集）
hoare-logic —— 编译器层证明的逻辑基础
ssa —— 编译器证明里寄存器分配的中间表示

一句话总结

VAMP = 把一颗有流水线、Tomasulo 乱序、IEEE 浮点、MMU 和 cache 的真处理器从门电路一路证到指令集，给 Verisoft 上层提供了「硬件可信」的地基。