riscv-formal
RISC-V Formal Verification Framework (by SymbioticEDA)
rp32
RISC-V processor with CPI=1 (every single instruction executed in a single clock cycle). (by jeras)
| riscv-formal | rp32 | |
|---|---|---|
| 10 | 3 | |
| 550 | 8 | |
| 3.6% | - | |
| 0.0 | 5.9 | |
| about 2 years ago | 7 months ago | |
| Verilog | SystemVerilog | |
| ISC License | Apache License 2.0 |
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.
rp32
Posts with mentions or reviews of rp32.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2022-06-30.
-
How to design a more elegant and simple instraction decoder
Here is my decoder: https://github.com/jeras/rp32/blob/master/hdl/rtl/riscv/riscv_isa_i_pkg.sv
- Mapping compressed 'C' instructions to their 32b counterparts.
-
Is a single cycle CPU of any use besides learning?
I am writing a RISC-V core with a strict IPC=1 (instructions per cycle). One piece is still in my mind, but the CPU is already passing instruction set tests.https://github.com/jeras/rp32The code was not properly synthesized yet, and there is almost no documentation, if you wish to use anything, but do not know how to, you can ask for help as a GitHub issue. But I do not know how much time I will have to answer.
What are some alternatives?
When comparing riscv-formal and rp32 you can also consider the following projects:
riscv-arch-test
cheshire - A minimal Linux-capable 64-bit RISC-V SoC built around CVA6
lion - Where Lions Roam: RISC-V on the VELDT
friscv - RISCV CPU implementation in SystemVerilog
riscv-tests
ibex - Ibex is a small 32 bit RISC-V CPU core, previously known as zero-riscy.
Cores-VeeR-EH1 - VeeR EH1 core
autofpga - A utility for Composing FPGA designs from Peripherals
neorv32 - :rocket: A tiny, customizable and extensible MCU-class 32-bit RISC-V soft-core CPU and microcontroller-like SoC written in platform-independent VHDL.
openarty - An Open Source configuration of the Arty platform
simple-riscv - A simple three-stage RISC-V CPU