Kami
Hardware designer
A Coq-based DSL for designing and verifying hardware systems
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
198 stars
73 watching
11 forks
Language: Coq
last commit: about 5 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
| sifive/prockami | Formal verification and implementation of RISC-V processor designs using Coq. | 22 |
 mit-plv/kami | A platform for high-level parametric hardware specification and modular verification | 143 |
| mit-plv/koika | A formal language for designing and verifying rule-based hardware systems | 143 |
 janestreet/hardcaml | A comprehensive OCaml library and toolset for designing, testing, and simulating digital hardware | 677 |
 nickmqb/wyre | A tool for designing and implementing digital hardware using a concise, typed language that compiles to Verilog | 106 |
 sylefeb/silice | A hardware description language that simplifies designing parallel and pipelined algorithms into FPGA hardware | 1,326 |
 bensampson5/libsv | A SystemVerilog digital hardware IP library with automated testbenches and continuous integration | 23 |
 cpc/openasip | A toolset for designing and programming customized co-processors with a focus on flexibility and customizability | 147 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 351 |
 magmide/magmide | Creating a programming language and ecosystem to make formal verification and provably correct software development practical and mainstream for working software engineers. | 810 |
 tchajed/iris-simp-lang | Instantiates a simple programming language with Iris to verify concurrent separation logic programs | 49 |
 imdea-software/fcsl-pcm | A formalisation of Partial Commutative Monoids (PCMs) for verification of concurrent programs. | 26 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
 siliconcompiler/lambdalib | A modular hardware abstraction library for designing and implementing complex digital systems | 23 |
 philzook58/nand2coq | An educational project building a formally verified version of the Nand 2 Tetris course using Coq and other formal tools. | 54 |