Kami is an umbrella term used to denote the following: . A Coq-based DSL for writing hardware designs . A compiler for translating said hardware designs into Verilog . A simulator for said hardware designs, by generating an executable in Haskell, using user-defined functions to drive inputs and examine outputs for the hardware design . A formal definition of the semantics of the DSL in Coq, including a definition of whether one design implements another simpler design, i.e. whether an implementation adheres to its specification . A set of theorems or properties about said semantics, formally proven in Coq . A set of tactics for formally proving that an implementation adhere to its specification
In Kami, one can write generators, i.e. functions that generate hardware when its parameters are specified, and can prove that the generators are correct with respect to their specification. Unlike traditional model-checking based approaches, the ability to prove theorems involving higher-order logic in Coq enables one to easily prove equivalence between a generator and its specification.
The semantics of Kami was inspired by Bluespec SystemVerilog. The original version of Kami was developed in MIT. Based on the experience of developing and using Kami at MIT, it was rewritten at SiFive to make it practical to build provably correct chips.
Any hardware block or module is written as a set of registers representing the state of the block, and a set of rules. The behavior of the module is represented by a sequence of execution of rules. Rules execute by reading and writing the state atomically, i.e. when one rule is executing, no other rule executes. During its execution, a rule can also interact with the external world by calling methods, to which the rule supplies arguments (an output from the module), and takes back the result returned by the external world (an input to the module). Once a rule finishes execution, another rule is picked non-deterministically and is executed, and so on.
A module A is said to implement a specification module B if,
during every rule execution in A, if the rule calls any methods,
then these methods (along with their arguments and return values) are
the same as those called by some rule execution in B, and this
property holds for every sequence of rule executions in A. Note that
the return values are functions of the external world; we assume that
the same value can be returned by the external world if the same
method is called with the same argument in both A and B. The
methods along with their arguments and return values that are called
in a rule’s execution are called a label, and the sequence of labels
corresponding to the sequence of rule execution is called a trace.
The above definition of A implementing B can be rephrased as
follows: any trace that can be produced by A can also be produced by
B. We call this property TraceInclusion.
While the above semantics cover most of the behavior of Kami modules, it is not complete. We will be discussing the last bit of the semantics towards the end of this article.
The syntax of Kami is designed to simply provide a way to represent a
set of registers (with optional initial values), and a set of rules.
The rules are written as actions which read or write registers, call
methods, deal with predicates (i.e. if then else), etc. The module
exampleModule in SyntaxEx.v shows an
example featuring all the syntactic components involved in writing a
module, including writing every possible expression, action,
register initialization and rule. The comments in the file give an
informal specification of what each syntactic construct does.
Notice that actions and let-expressions are essentially are
ASTs written in
Gallina. So, one can construct these actions or let-expressions
separately as Gallina terms without having to be inside a Kami
module. This way, one can write generators that produce actions or
let-expressions that can be composed in multiple ways into a module.
GallinaActionEx.v shows how to write
such Gallina terms. Notice the use of a strange parameter
ty: Kind → Type. This is used to get parametric ASTs that allow us
to use the same AST for synthesizing circuits as well as for
proofs. Read a tiny example, PhoasEx.v and
Parametric
Higher Order Abstract Syntax (PHOAS) paper to understand what PHOAS
means. While understanding PHOAS is useful, one need not understand
the concepts to build actions and let-expressions in Kami. Instead,
one can view supplying ty: Kind → Types as boiler plate code, and
write types for expressions as k @# ty, let-expressions as k ## ty
and actions as ActionT ty k (k represents the Kami type represented
by these entities).
TacticsEx.v showcases how some of the Coq tactics developed
in the Kami framework can be used to simplify the proof of TraceInclusion
between two modules. The documentation for this is work in progress.