The Science of Deep Specification

Kami: Digital Hardware Programming and Verification in Coq

Kami is a library that turns Coq into an IDE for digital hardware development, based on a clean-slate reimplementation of a core of the Bluespec language. We span the gap from mathematical specifications to hardware circuit descriptions (RTL netlists). We support specifying, implementing, verifying, and compiling hardware, reasoning at a high level about particular hardware components but in the end deriving first-principles Coq theorems about circuits. No part of Kami need be trusted beside the formalization of low-level (Verilog-style) circuit descriptions; all other aspects have end-to-end correctness proofs checked by Coq. Hardware designs are broken into separately verified modules, reasoned about with a novel take on labeled transition systems. Furthermore, Coq provides a natural and expressive platform for metaprogramming, or building verified circuit generators, as for a memory caching system autogenerated for a particular shape of cache hierarchy, or a CPU generated given a number of concurrent cores as input.

Kami project website