search

sifive / Kami

Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT
Apache License 2.0
197 stars 11 forks source link

readme

:toc:

= Kami -- A Coq-based DSL for specifying and proving hardware designs

== What is Kami? Kami is an umbrella term used to denote the following: . A https://en.wikipedia.org/wiki/Coq[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 http://wiki.bluespec.com/[Bluespec SystemVerilog]. The original version of http://plv.csail.mit.edu/kami/papers/icfp17.pdf[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.

== Semantics of Kami: an informal overview 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.

== Syntax of Kami 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 link:Tutorial/SyntaxEx.v[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 https://en.wikipedia.org/wiki/Abstract_syntax_tree[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. link:Tutorial/GallinaActionEx.v[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, link:Tutorial/PhoasEx.v[PhoasEx.v] and http://adam.chlipala.net/papers/PhoasICFP08/PhoasICFP08.pdf[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).

== Proving implementations using Kami link:Tutorial/TacticsEx.v[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.