kami
Hardware specification platform
A platform for high-level parametric hardware specification and modular verification
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
143 stars
14 watching
24 forks
Language: Coq
last commit: 5 months ago
Linked from 2 awesome lists
bluespeccoqhardware-description-languagehardware-verificationproof-assistant
aolofsson/awesome-opensource-hardware
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
| mit-plv/koika | A formal language for designing and verifying rule-based hardware systems | 143 |
 sifive/kami | A Coq-based DSL for designing and verifying hardware systems | 198 |
| sifive/prockami | Formal verification and implementation of RISC-V processor designs using Coq. | 22 |
| mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
| mit-plv/fiat | A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications | 149 |
| mit-plv/riscv-coq | An implementation of the RISC-V instruction set specification in Coq | 110 |
 ml4tp/gamepad | A platform that exposes Coq proofs to machine learning algorithms | 72 |
| mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 42 |
| mit-plv/bbv | A repository unifying bit vector definitions and lemmas across multiple Coq projects. | 27 |
 vlsi-eda/poc | Provides VHDL implementations of common hardware functions and a Python-based infrastructure for simulation and synthesis. | 554 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
 rdaly525/coreir | Builds hardware descriptions into executable code using an LLVM-style compiler framework. | 101 |
 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 |
 philtomson/rhdl | A Ruby language and framework for designing and describing digital hardware systems | 14 |