ProcKami

Processor simulator

Formal verification and implementation of RISC-V processor designs using Coq.

Kami based processor implementations and specifications

GitHub

22 stars
61 watching
3 forks
Language: Coq
last commit: over 4 years ago
coqformal-verificationhardwarehardware-designsriscvriscv-simulator

Related projects:

Repository Description Stars
sifive/kami A Coq-based DSL for designing and verifying hardware systems 197
mit-plv/kami A platform for high-level parametric hardware specification and modular verification 142
openhwgroup/core-v-verif Functional verification project for RISC-V cores 446
chipsalliance/riscv-dv An instruction generator for RISC-V processor verification 1,020
mit-plv/riscv-coq An implementation of the RISC-V instruction set specification in Coq 109
mit-plv/koika A formal language for designing and verifying rule-based hardware systems 140
mariusmm/risc-v-tlm A RISC-V processor simulator with SystemC and TLM-2 support for various instruction sets and peripherals. 276
mit-plv/bedrock Automated verification of higher-order programs using separation logic 57
havivha/nand2tetris An implementation of a complete computer using Nand gates on up as described in the book 'The Elements of Computing Systems' 419
cpitclaudel/company-coq An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software 354
philzook58/nand2coq An educational project building a formally verified version of the Nand 2 Tetris course using Coq and other formal tools. 54
riscv/sail-riscv A comprehensive formal specification of a RISC-V processor architecture using the Sail language 461
kev-cam/v2k-top A software framework for parsing and simulating digital circuits described in Verilog and C++ languages. 7
olofk/serv An award-winning RISC-V CPU designed for low-power and area-efficient designs 1,442
gem5/gem5 A modular simulator for evaluating computer system architectures and designs 1,692