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

是什么

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

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

它最响亮的成果：第一个被完整形式化证明的 RISC-V 流水线处理器。从 ISA 规约一路证到 Verilog 网表。在它之前，“形式化证明的硬件”基本只能给到 AMBA 总线协议这种规模；Kami 把上限拉到了一颗能跑程序的真 CPU。

为什么重要

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

为什么 Intel Pentium FDIV bug（1994 年浮点除法错误，召回 4.75 亿美元）那种硬件 bug 可以彻底避免
为什么 Spectre / Meltdown（2018）这类微架构级别的漏洞极难发现——传统验证只看功能不看流水线交互
为什么 ARM 自己也只能形式化总线协议这种”小例子”，而完整流水线 CPU 之前没人证完
为什么硬件验证业界还在用 SystemVerilog Assertions + 仿真而不是数学证明——成本和工具栈都缺

核心要点

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

rule 是原子单元：电路里每个动作都是一条”守卫规则”——条件成立就整条原子跑完，否则不跑。类比交通灯路口，每个绿灯周期是一条 rule。这个抽象抄自 MIT 自家的 Bluespec。
模块可参数化：缓存几路、流水线几级、寄存器多宽，全是 Coq 参数。一次证明覆盖所有合法参数——这点是 Verilog 做不到的。
精化（refinement）是证明骨架：高层规约（“这个 CPU 等价于一条一条顺序执行 ISA”）⊑ 流水线实现。分层证：每加一层（取指、译码、bypass、cache），都用一次精化把新优化”消掉”。

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

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

为什么这条链能成立？因为每一段都有”语义保持”的证明：Kami 模块的 rule 语义和提取后的 Bluespec rule 一一对应；Bluespec 到 Verilog 这一步虽然没在 Coq 里证，但 Bluespec 编译器自身被工业用了 15 年，可信度比手写 RTL 高。

可观察行为 vs 内部状态

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

实践案例

案例 1：rule 抽象怎么避免数据冒险

经典流水线问题：第 1 拍写 r1，第 3 拍才能读到。如果第 2 拍另一条指令读 r1，就错。Kami 里把 bypass（直通转发）写成一条 rule：当”前一拍写、本拍读”成立时，rule 触发，把写的值直接喂给读端。

证明义务变成”有了这条 rule，行为等价于无流水的顺序执行”。Coq 里一行 refines 引理就把这层证完。这种风格的好处是：bypass 的证明和分支预测、cache miss 处理是解耦的——每加一条新优化只需补一条精化引理，不用重证整体。

案例 2：参数化 cache 一次证多种配置

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

一份代码、一次证明，覆盖直接映射 / 2 路 / 4 路 / 8 路。Verilog 里要做这个只能复制粘贴或生成器+测试，证明做不到”对所有参数都成立”。Kami 这一招源自 Coq 的依赖类型——numWays: nat 既是数据也是类型层面的索引，证明里直接对它做归纳。

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

论文里把 RV32I 子集的 4 级流水线（取指 / 译码 / 执行 / 写回 + bypass + 简单 cache）写成 Kami 模块，12K 行 Coq 证明最后得出：

PipelinedRV32I  ⊑  SequentialISASpec

读作”流水线实现精化于顺序 ISA 规约”——意思是流水线对外可观察的行为，等价于一条条顺序跑指令。把它跑到 FPGA 上做 echo / Fibonacci 一类小程序，证明 + 实物两端都对得上。

踩过的坑

证明工程量极大：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 把同类思想搬到硬件