koika
Hardware design language
A formal language for designing and verifying rule-based hardware systems
A core language for rule-based hardware design 🦑
143 stars
24 watching
11 forks
Language: Coq
last commit: about 1 year ago compilationcoqformal-methodshardware-description-languageprogramming-languagessemantics
Related projects:
| Repository | Description | Stars |
|---|---|---|
| mit-plv/kami | A platform for high-level parametric hardware specification and modular verification | 143 |
| mit-plv/rupicola | A toolkit for compiling functional programs into imperative code for performance-critical applications | 51 |
 sifive/kami | A Coq-based DSL for designing and verifying hardware systems | 198 |
| mit-plv/fiat | A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications | 149 |
| mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
| sifive/prockami | Formal verification and implementation of RISC-V processor designs using Coq. | 22 |
 fabianschuiki/llhd | An intermediate representation language and simulator for digital circuit descriptions, aiming to simplify the development of EDA tools. | 397 |
| mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 42 |
| mit-plv/riscv-coq | An implementation of the RISC-V instruction set specification in Coq | 110 |
| mit-plv/riscv-semantics | A formal specification of the RISC-V instruction set architecture in Haskell | 159 |
 vlsi-eda/poc | Provides VHDL implementations of common hardware functions and a Python-based infrastructure for simulation and synthesis. | 554 |
 philtomson/rhdl | A Ruby language and framework for designing and describing digital hardware systems | 14 |
 clash-lang/clash-compiler | A Haskell-based compiler for hardware description languages like VHDL, Verilog, and SystemVerilog. | 1,451 |
 kit-ty-kate/labrys | A compiler for a toy language based on LLVM that implements the System Fω type-system | 103 |
 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 |