一句话：Kami 是 Coq 库，支持以 Bluespec 风格高层参数化地规范、实现并模块化验证硬件设计。
编程语言研究界已习惯在证明助手中借助归纳、代数化简和重写来验证函数式程序。本文提出 Kami，一个 Coq 库，将类似的表达力与模块化推理能力引入用 Bluespec 风格表达的硬件设计。研究者可在 Coq 内完整地规范、实现和验证真实设计，并最终自动提取到面向 FPGA 的流水线中。其方法基于标签迁移系统，并通过一个案例研究进行评估：验证一个无限族多核系统，这些系统具有缓存一致的共享内存以及实现 RISC-V 基础整数子集的流水线核心。
It has become fairly standard in the programming-languages research world to verify functional programs in proof assistants using induction, algebraic simplification, and rewriting. In this paper, we introduce Kami, a Coq library that enables similar expressive and modular reasoning for hardware designs expressed in the style of the Bluespec language. We can specify, implement, and verify realistic designs entirely within Coq, ending with automatic extraction into a pipeline that bottoms out in FPGAs. Our methodology, using labeled transition systems, has been evaluated in a case study verifying an infinite family of multicore systems, with cache-coherent shared memory and pipelined cores implementing (the base integer subset of) the RISC-V instruction set.
@article{ChoiVSCA17,
title = {Kami: a platform for high-level parametric hardware specification and its modular verification},
author = {Joonwon Choi and Muralidaran Vijayaraghavan and Benjamin Sherman and Adam Chlipala and Arvind},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110268}
}