mit-plv / Riscv Coq
Licence: bsd-3-clause
RISC-V Specification in Coq
Stars: ✭ 63
Labels
Projects that are alternatives of or similar to Riscv Coq
Silveroak
Formal specification and verification of hardware, especially for security and privacy.
Stars: ✭ 51 (-19.05%)
Mutual labels: coq
Freespec
A framework for implementing and certifying impure computations in Coq
Stars: ✭ 41 (-34.92%)
Mutual labels: coq
Scala Escape
A compiler plug-in to control object lifetimes in Scala
Stars: ✭ 60 (-4.76%)
Mutual labels: coq
Jt89
sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility
Stars: ✭ 14 (-77.78%)
Mutual labels: coq
Certint
A Certified Interpreter for ML with Structural Polymorphism
Stars: ✭ 39 (-38.1%)
Mutual labels: coq
RISC-V Specification in Coq
Generated from the RISCV Semantics in Haskell using hs-to-coq, with some manually written Coq files too. Currently, the architectures RV32I and RV64I with any combination of the extensions A and M are supported.
Build
You will need Coq 8.9 or master.
riscv-coq depends on the coqutil library. You can get this dependency and build the project using the following commands:
git clone https://github.com/mit-plv/coqutil.git
git clone https://github.com/mit-plv/riscv-coq.git
make -C coqutil
cd riscv-coq/
make
If it doesn't build
If something doesn't work, you could try to do exactly the same as bedrock2 does, which uses riscv-coq as a dependency and has Travis Continuous Integration, so if you pick a commit with a green tick there, you can be sure to have a working version.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].