Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
The work
| Authors | Joonwon Choi; Muralidaran Vijayaraghavan; Benjamin Sherman; Adam Chlipala; Arvind |
|---|---|
| Editors | |
| Type | article |
| Year | 2017 |
| Citekey | choi2017kami |
Where it appeared
| Published in | Proceedings of the ACM on Programming Languages |
|---|---|
| Volume | 1 |
| Issue | ICFP |
| Pages | 1--30 |
Identifiers
| DOI | 10.1145/3110268 |
|---|
Access
| Landing page | https://adam.chlipala.net/papers/KamiICFP17/KamiICFP17.pdf |
|---|
Related
| Distinct from | baty2024formal |
|---|---|
| Distinct from | bourgeat2025making |
| Distinct from | chen1996verification |
| Distinct from | clarke1986automatic |
| Distinct from | gammie2013synchronous |
| Distinct from | jacobi2005automatic |
| Distinct from | kurze2026nocout |
| Distinct from | lau2026granite |
| Distinct from | oleary1999formally |
| Distinct from | oleary2013relational |
From bibtex.
Abstract
It has become fairly standard in programming-languages research to verify functional programs in proof assistants using induction, algebraic simplification, and rewriting. In this paper, we introduce Kami, a Coq library that uses labeled transition systems to enable 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 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.
A copy is held
pdf, 963.7 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-17 05:13 UTC |
| Approved by | a person 2026-09-17 16:59 UTC |
Cite it as
@article{choi2017kami,
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},
year = {2017},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
pages = {1--30},
doi = {10.1145/3110268},
}
This record lives at https://refs.drheap.org/choi2017kami/ and will keep doing so.