Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
Directory content
./: Contains the source code for syntax, semantics, theorems/properties and
proof automation for Kami.
Lib: Contains the generic library files that we developed for Kami, extending
the standard Coq library, e.g. bit-vectors, decidable finite maps with strings
as keys, etc.
Ex: Contains basic examples and tutorials.
Ext: Files needed to extract designs developed in Kami into Bluespec
Ocaml: Contains the files to pretty-print the OCaml code extracted from Coq.
Requirements
To Verify Kami modules
Coq 8.12.x with $PATH containing the standard Coq binaries
To Generate Bluespec programs
OCaml 4.0.4 (with $PATH containing the standard OCaml binaries)
Vivado 2015.4 (with $PATH containing the Bluespec binaries)
Xilinx Virtex-7 VC707 Evaluation Kit FPGA
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].