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
156 stars
24 watching
16 forks
Language: Haskell
last commit: over 1 year ago Related projects:
| Repository | Description | Stars |
|---|---|---|
| mit-plv/riscv-coq | An implementation of the RISC-V instruction set specification in Coq | 109 |
 riscv/sail-riscv | A comprehensive formal specification of a RISC-V processor architecture using the Sail language | 461 |
| 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,020 |
 standardsemiconductor/lion | Develops a formally verified RISC-V processor core using Haskell | 249 |
 rust-embedded/riscv | Provides a set of Rust libraries and tools for accessing and interacting with RISC-V microcontrollers. | 852 |
 symbioticeda/riscv-formal | A framework for formally verifying RISC-V processors by providing a processor-independent formal description and testbenches. | 585 |
 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 | 140 |
| mit-plv/fiat | A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications | 147 |
 lekkit/rvvm | An emulator and virtual machine for the RISC-V instruction set architecture. | 936 |
| mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 41 |
 haskell/lsp | A Haskell implementation of the Microsoft Language Server Protocol | 366 |
 olofk/serv | An award-winning RISC-V CPU designed for low-power and area-efficient designs | 1,442 |
| mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |