A Coq framework to support implementing, specifying, verifying, and compiling Bluespec-style hardware components with high developer productivity.
Overview
Kami is a Coq framework to support implementing, specifying, verifying, and compiling Bluespec-style hardware components with high developer productivity. The core of the approach is modular proofs of hardware components. We aim for specifications and proofs that mirror the modular decomposition of a large hardware system into simpler parts. We also intend to support techniques for machine-checked correctness proofs of key synthesis algorithms that translate high-level hardware designs into low-level circuit descriptions.
The name Kami comes from a Shinto word for nature spirits (roughly).
Team
Adam ChlipalaDownloads
Publications
Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
paper bibtex
,
,
,
,
.
Kami: A Platform for High-Level Parametric Hardware Specification
and Its Modular Verification. Proceedings of the 22nd ACM SIGPLAN
International Conference on Functional Programming
(ICFP'17). September 2017.
,
,
,
Nirav Dave.
Modular Deductive Verification of Multiprocessor Hardware
Designs. Proceedings of the 27th International Conference on
Computer Aided Verification (CAV'15). July 2015.