Kami — 在 Coq 里造硬件并自动编译到 Verilog

待复核

是什么

Kami 是 MIT 团队（Choi、Vijayaraghavan、Sherman、Chlipala、Arvind）做的一个硬件描述语言，但不是写在专门工具里——它就长在 Coq 定理证明器内部。你在 Coq 里描述一段电路（比如 CPU 流水线），同时在 Coq 里证明这段电路满足某个规约，最后让工具把 Coq 描述编译成真正的 Verilog（FPGA / 流片都能用）。

日常类比：像在 LEGO 说明书里同时写两件事——组装步骤、和”拼出来一定能跑”的数学证明，最后机器再把组装步骤翻译成实物零件清单。说明书本身就是证明，不是写完后再补写一份。

它最响亮的成果：第一个被完整形式化证明的 RISC-V 流水线处理器（RISC-V = 一种开源指令集；流水线 = 多条指令重叠执行）。证明边界是：从 ISA 规约（指令集该做什么）精化到 Kami 模块，再提取到 Bluespec；最后由 Bluespec 编译器生成 Verilog 供 FPGA / 流片。Bluespec→Verilog 这一跳不在 Coq 证明里——开头若说”证到网表”会过强。在它之前，“形式化证明的硬件”多停在 AMBA 总线协议这类规模；Kami 把上限拉到一颗能跑小程序的 CPU 核。

为什么重要

不理解 Kami 这种工作，下面这些事都没法解释：

为什么 Intel Pentium FDIV bug（1994 年浮点除法错误，召回 4.75 亿美元）那种功能硬件 bug，理论上可用端到端证明压掉
为什么流水线、旁路、缓存一叠上去，单靠仿真很难穷尽交互——微架构正确性验证成本陡增（Spectre / Meltdown 是侧信道另一条线，Kami 主攻的是功能精化，不直接覆盖推测执行攻击）
为什么业界长期把”完整流水线 CPU 的端到端证明”当成难事，而总线协议级形式化相对更常见
为什么硬件验证仍大量用 SystemVerilog Assertions + 仿真而不是数学证明——成本和工具栈都缺

核心要点

Kami 把硬件设计拆成三个层次：

rule 是原子单元：电路里每个动作都是一条”守卫规则”——条件成立就整条原子跑完，否则不跑。类比交通灯路口，每个绿灯周期是一条 rule。这个抽象来自 Bluespec（MIT 系的 rule 风格硬件语言，工业里用来写可综合 RTL）。
模块可参数化：缓存几路、流水线几级、寄存器多宽，全是 Coq 参数。一次证明覆盖所有合法参数——这点是 Verilog 做不到的。
精化（refinement）是证明骨架：人话版——证明”花哨实现”对外看起来仍等于”傻瓜顺序版”。记号 A ⊑ B 读作”A 精化于 B / A 的可观察行为不超出 B”。高层规约是”CPU ≡ 一条条顺序执行 ISA”；每加一层（取指、译码、bypass、cache），就用一次精化把新优化”消掉”。

这一套加上一条编译流水线：

Coq Kami 模块 → 提取到 Bluespec → Bluespec 编译器 → Verilog

为什么这条链能用？Kami→Bluespec 提取有”语义保持”论证（rule 一一对应）；Bluespec→Verilog 不在 Coq 里证，可信度来自 Bluespec 编译器多年工业使用，仍弱于端到端机器检查证明。

可观察行为 vs 内部状态

精化的关键是只比对外可观察行为。流水线内部多了寄存器、bypass 路径，但只要”对外发出的内存访问序列、写回的寄存器值”和顺序执行 ISA 一致，就算等价。这把内部优化的自由度全释放出来——你可以随便改流水级数、加分支预测，只要可观察行为不变就还能复用证明。

实践案例

案例 1：bypass rule 怎么消掉数据冒险（跟读 4 步）

经典流水线问题：第 1 拍写寄存器 r1，第 3 拍才能从寄存器堆读到；若第 2 拍另一条指令读 r1，就会读到旧值。

在 Kami 里把 bypass（旁路/直通转发）写成一条 rule：守卫是”前一拍写、本拍读同一寄存器”。
rule 触发时，不走寄存器堆，直接把写端的值喂给读端。
证明义务变成一句人话：加上这条 rule 后，对外行为仍 ⊑ 无流水的顺序执行。
在 Coq 里对这一层写 refines 引理；bypass 与分支预测、cache miss 解耦——新优化只补一条精化，不必重证整核。

案例 2：参数化 cache（教学示意，非粘贴即跑）

下面不是完整可编译 Kami 源码，只示意”参数出现在类型里”：

Definition mkCache (numWays: nat) (lineSize: nat) := ...

跟读：打开 mit-plv/kami → 找 cache / processor 示例 → 对照 numWays 这类参数如何同时出现在实现与证明里。一份证明可覆盖直接映射 / 2 路 / 4 路；Verilog 侧通常只能复制粘贴或生成器+测试。

案例 3：4 级 RISC-V 流水线证完

论文把 RV32I（RISC-V 的 32 位整数基础子集）做成 4 级流水线（取指 / 译码 / 执行 / 写回 + bypass + 简单 cache），约 12K 行 Coq 得到：

PipelinedRV32I  ⊑  SequentialISASpec

读作：流水线实现精化于顺序 ISA 规约——对外可观察行为等价于一条条顺序跑指令。再综合到 FPGA 跑 echo / Fibonacci 等小程序，证明结论与实物行为对齐（仍记住：最终 Verilog 来自 Bluespec 编译，不在 Coq 证明边界内）。

踩过的坑

证明工程量极大：12K 行 Coq 证一个简化流水线。学界乐观估计现代乱序 CPU 要 100 倍。这就是为什么至今没人证完 ARM Cortex-A76。
生成的 Verilog 性能差：Kami → Bluespec → Verilog 这条链每一步都保守。同样规格的 CPU，手写 Verilog 频率/面积都更好。Kami 现阶段是”研究 / 高安全场景”用，不是”日常 SoC”用。
Coq 学习曲线陡：写 Kami 等于学三件事——硬件、Coq、Bluespec rule 语义。任何一件不熟都跑不动。
物理时序没覆盖：Kami 证的是功能正确，不是”能在 1 GHz 跑”。setup/hold、CDC（跨时钟域）这些还得靠传统 EDA 流程。
异常/中断尚未完整：论文里的 RV32I 不含 trap、interrupt、virtual memory。这些是真实 CPU 最容易出 bug 的地方，Kami 后续工作（如 riscv-coq）才补上一部分。
rule 调度有性能税：Bluespec 编译器为了保证 rule 原子性，会自动插入互斥逻辑。两条同周期都想跑的 rule 会被串行化，导致吞吐量比手写 RTL 低。证明友好 ↔ 性能损失，目前没有甜点配置。
测试 vs 证明的心智切换：硬件工程师习惯写 testbench 跑波形看波形，Kami 让你写 forall states, P state 这类全称命题。两套思维方式完全不同，团队上手 6 个月起步。

适用 vs 不适用场景

适用：

安全攸关芯片（航天、加密协处理器、TEE）——bug 代价远高于证明成本
教学：想让学生看见”硬件也能数学证明”，理解 ISA 与微架构的层次差
研究新流水线优化时，先在 Kami 里证明等价再写 RTL，避免设计走偏
验证小型加速器（FFT、AES、SHA）的等价性——规模小，证明负担可控
标准制定：用 Kami 写出 RISC-V 子集的”可执行黄金模型”，作为各家实现的参照

不适用：

量产消费级 SoC——成本与时间不允许，市场窗口比证明完成更早关闭
模拟电路 / 异步电路——Kami 是同步数字，无法描述时钟域以外的行为
需要榨干频率面积的高性能 GPU / TPU——生成的 Verilog 留不出余量
团队没有 Coq 经验——投入产出比极差，前 6 个月几乎产不出可证电路
快速迭代的早期原型——证明追不上需求变更，反而拖慢节奏

历史小故事（可跳过）

1990 年代：Arvind 在 MIT 推动 Term Rewriting Systems 用于硬件。最早的”rule 是原子单元”思想从这里来。
2003 年：Bluespec（Arvind 创立的公司）推出基于 rule 的硬件 DSL，被业界认为”太学术”。
2008 年：Adam Chlipala 加入 MIT，开始用 Coq 做编译器、操作系统的形式化（Bedrock 项目）。
2010 年代：Chlipala 写《Certified Programming with Dependent Types》。学生 Choi 把 Bluespec rule 语义嵌入 Coq，原型跑通。
2017 年：ICFP 论文发表 Kami，配套的 RISC-V 流水线证明跑通。这是首个端到端证明的现代 CPU 流水线。
2020 后：bedrock2、riscv-coq、Lutsig 等后续把 Kami 思路推广到更大设计；MIT 团队还在做 SoC 总线、cache 一致性的形式化。
当下：DARPA SSITH 等项目把 Kami 列为”可信硬件”参考路径之一，但生产芯片仍未采用。

学到什么

硬件也能数学证明——之前大家以为只有”总线协议”这种小东西能证，Kami 证明流水线 CPU 也能。
rule 抽象比 RTL 更适合证明：原子规则的语义干净，refinement 链好搭。RTL 的 always @(posedge clk) 本身就难做形式语义。
参数化 + 一次证明 比”枚举测试”强一个数量级——Verilog 永远做不到对所有参数都成立。
理论 → 工具链 → 杀手级 demo 缺一不可：rule 语义（理论）+ Coq 嵌入 + Bluespec 编译（工具）+ RISC-V 流水线（demo），三件齐了才被业界看见。
可证明性是一种约束：选 rule 而非 RTL、选精化而非穷举测试、选参数化而非复制粘贴——这些选择让证明可行，也让设计风格更受限。它换来的是”对所有输入、所有参数、所有调度都成立”的承诺。

与传统硬件验证的对比

维度	传统流程（SystemVerilog + 仿真）	Kami
描述语言	RTL（Verilog/VHDL）	Coq 内嵌的 rule DSL
验证手段	测试用例 + 形式断言 + 覆盖率	数学证明，对所有输入成立
参数化	复制粘贴或脚本生成器	一次证明覆盖所有合法参数
流水线优化	仿真见招拆招	每条优化对应一条精化引理
输出	直接 Verilog	Coq 模块 → Bluespec → Verilog
团队门槛	硬件工程师即可	需要 Coq + Bluespec + 硬件三栈
适合规模	任意	中小型核心 + 加速器

这张表说明 Kami 不是要替代传统流程，而是在”安全 / 标准 / 教学”这些细分场景里，提供另一种保证强度更高的路径。它和仿真不冲突——很多团队把 Kami 当作 ISA 标准的可执行参照，仿真照常做。

关联

acl2-2000 —— 工业硬件验证另一条路线（AMD K5 用过），不嵌 Coq 而用 Lisp 自带 prover
compcert —— “形式化证明的编译器” → Kami 是”形式化证明的硬件”
coq —— Kami 的宿主，Kami 模块就是 Coq 项
hyperkernel-2017 —— 同年代的”全栈形式化”思路，但目标是 OS 内核而非 CPU
ironfleet-2015 —— 用 Dafny 做分布式系统验证；Kami 把同类思想搬到硬件

反向链接

（暂无反向链接）