riscv-semantics
RISC-V semantics
A formal specification of the RISC-V instruction set architecture in Haskell
A formal semantics of the RISC-V ISA in Haskell
159 stars
24 watching
16 forks
Language: Haskell
last commit: about 2 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
| mit-plv/riscv-coq | An implementation of the RISC-V instruction set specification in Coq | 110 |
 riscv/sail-riscv | A comprehensive formal specification of a RISC-V processor architecture using the Sail language | 480 |
| mit-plv/bbv | A repository unifying bit vector definitions and lemmas across multiple Coq projects. | 27 |
 chipsalliance/riscv-dv | An instruction generator for RISC-V processor verification | 1,036 |
 standardsemiconductor/lion | Develops a formally verified RISC-V processor core using Haskell | 249 |
 rust-embedded/riscv | Provides low-level access and interfaces for writing software on RISC-V microcontrollers. | 874 |
 symbioticeda/riscv-formal | A framework for formally verifying RISC-V processors by providing a processor-independent formal description and testbenches. | 589 |
 mrlsd/riscv-fs | A F# implementation of the RISC-V Instruction Set Architecture | 282 |
| mit-plv/koika | A formal language for designing and verifying rule-based hardware systems | 143 |
| mit-plv/fiat | A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications | 149 |
 lekkit/rvvm | An emulator and virtual machine for the RISC-V instruction set architecture. | 953 |
| mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 42 |
 haskell/lsp | A Haskell implementation of the Microsoft Language Server Protocol | 371 |
 olofk/serv | An award-winning RISC-V CPU designed for low-power and area-efficient designs | 1,457 |
| mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |