riscv-formal
RISC-V Formal Verification Framework (by SymbioticEDA)
planckRV32I
Core based on RV32I ISA (by Tersonous)
| riscv-formal | planckRV32I | |
|---|---|---|
| 10 | 1 | |
| 550 | 4 | |
| 3.6% | - | |
| 0.0 | 6.8 | |
| about 2 years ago | over 3 years ago | |
| Verilog | ||
| ISC License | BSD 3-clause "New" or "Revised" License |
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
riscv-formal
Posts with mentions or reviews of riscv-formal.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2023-12-10.
-
RISC-V simulator
You might be able to hook up your simulator to risc v-formal https://github.com/SymbioticEDA/riscv-formal
- how is to use symbiflow in my fpga projects.
-
Machine readable specifications at scale
Then we have RISC, which wrote their own formal verification toolchain here. They just generate Verilog with a Python script. AFAICT this would be really hard to adapt to an assembler. Fortunately the ISA is simple to implement.
- Looking for an rv32i asm program that covers all possible scenarios of all instructions for testing
- Is a single cycle CPU of any use besides learning?
- When to use Formal Verification vs Simulation?
-
Where Lions Roam: RISC-V on the VELDT
Your question is certainly not dumb; on the contrary, it is very important! I suppose the developers are responsible for verifying the formal verifier and ensuring it covers the spec. Maybe there is a way to formally verify the formal verifier? Either way, I must give a shout out to the riscv-formal project and its contributors; the project was instrumental to the development of Lion.
Not trying to put words in your mouth, but I do want to clarify something for this audience: the bound in the BMC done by the riscv-formal suite is on the number of cycles, not on the number of bits. Case in point, when you try to BMC the (M)ultiply extensions with the riscv-formal suite, you're actually not allowed to use multiplication because the state space blows up: https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/rvfi.md#alternative-arithmetic-operations
-
Any advices for my first RISC-V Core in Verilog ?
Use riscv-formal. It will save a ton of headaches trying to track down a bad instruction. It can generate a module that does checks on the fly during normal sims.
-
FPGA and Simulation tools for Risc-V design
I recommend SymbiYosys for formally testing your CPU before ever placing it into a simulation. You can use the riscv-formal property set to get you started, but I'd personally go for an inductive proof of some type and the riscv-formal property set may not get you that far.
planckRV32I
Posts with mentions or reviews of planckRV32I.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2021-02-05.
-
Any advices for my first RISC-V Core in Verilog ?
For now what i can tell is there : https://github.com/Tersonous/planckRV32I/blob/main/vriscv.png
What are some alternatives?
When comparing riscv-formal and planckRV32I you can also consider the following projects:
riscv-arch-test
lion - Where Lions Roam: RISC-V on the VELDT
rp32 - RISC-V processor with CPI=1 (every single instruction executed in a single clock cycle).
riscv-tests
Cores-VeeR-EH1 - VeeR EH1 core
autofpga - A utility for Composing FPGA designs from Peripherals
openarty - An Open Source configuration of the Arty platform
hs-arm - (Dis)assembler and analyzer generated from the machine-readable ARMv8.3-A specification
simple-riscv - A simple three-stage RISC-V CPU
X86-64-semantics - Semantics of x86-64 in K
VexRiscv - A FPGA friendly 32 bit RISC-V CPU implementation