koika
Hardware design language
A formal language for designing and verifying rule-based hardware systems
A core language for rule-based hardware design 🦑
140 stars
24 watching
9 forks
Language: Coq
last commit: about 1 month 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 | 142 |
| mit-plv/rupicola | A toolkit for compiling functional programs into imperative code for performance-critical applications | 50 |
 sifive/kami | A Coq-based DSL for designing and verifying hardware systems | 197 |
| mit-plv/fiat | A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications | 147 |
| 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 for digital circuit descriptions, enabling the creation of custom hardware design tools and simulators. | 396 |
| mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 41 |
| mit-plv/riscv-coq | An implementation of the RISC-V instruction set specification in Coq | 109 |
| mit-plv/riscv-semantics | A formal specification of the RISC-V instruction set architecture in Haskell | 156 |
 vlsi-eda/poc | Provides VHDL implementations of common hardware functions and a Python-based infrastructure for simulation and synthesis. | 551 |
 philtomson/rhdl | A Ruby-based language for describing digital hardware components and their behavior. | 14 |
 clash-lang/clash-compiler | A compiler that transforms high-level Haskell descriptions into synthesizable hardware descriptions. | 1,442 |
 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. | 812 |