openarty
An Open Source configuration of the Arty platform (by ZipCPU)
riscv-formal
RISC-V Formal Verification Framework (by SymbioticEDA)
openarty | riscv-formal | |
---|---|---|
6 | 10 | |
116 | 550 | |
- | 3.6% | |
0.0 | 0.0 | |
4 months ago | about 2 years ago | |
Verilog | Verilog | |
- | ISC 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.
openarty
Posts with mentions or reviews of openarty.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2023-06-11.
-
C++ Verification Testbench Best-Practice Resources?
I have built a lot of open-source C++ tooling for design verification. You can find a lot of my C++ models posted on my Github. Example C++ models include: UART, SPI/DSPI/QSPI Flash, SD-Card (SPI-based interface), VGA Video, Ethernet MDIO, PS/2 mouse, OLED display, SDRAM and more. (I've even simulated PLLs using C++ models ...) I have also written extensively about doing so at ZipCPU.com.
-
PPS detection/regeneration
The repo is the example design. It was used by software, though, that's not (currently) posted. A lot of math went into the coefficients as well--that's all in the software.
-
AXI Quad SPI 3.2 Flash programming scripts
Here's the flash controller repo I use. There's a flash controller in there for SPI, Dual SPI, and Quad SPI. The Dual and Quad SPI controllers need a device specific startup script to get them into the right mode. This script should be fairly well explained by the comments. You should find at least one of these controllers that works for you. More recent versions of the controller have a Wishbone arbiter within them -- they're just not checked in the repo yet. (DSPI, QSPI). This makes it so the design fully supports two two Wishbone ports: a config port by which you can send any value and the memory mapped read port. (You can't use both at the same time.)
-
Arty S7 - 2 different flash brands
You can compare my configuration file for the Spansion flash with my config file for the Micron flash to see that these are the only two hardware differences between the two
-
FPGA and Simulation tools for Risc-V design
I'd then recommend Verilator for simulation testing--but only after your formal design checking is complete. You can find online C++ models of a QSPI flash, RAM, and a serial port which should be good enough to get you going here. When you are ready for more permanent storage, there's also a decent C++ model of an SD card (SPI only).
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.
What are some alternatives?
When comparing openarty and riscv-formal you can also consider the following projects:
zipcpu - A small, light weight, RISC CPU soft core
riscv-arch-test
lion - Where Lions Roam: RISC-V on the VELDT
wbicapetwo - Wishbone to ICAPE interface conversion
rp32 - RISC-V processor with CPI=1 (every single instruction executed in a single clock cycle).
qspiflash - A set of Wishbone Controlled SPI Flash Controllers
riscv-tests
autofpga - A utility for Composing FPGA designs from Peripherals
Cores-VeeR-EH1 - VeeR EH1 core
wbuart32 - A simple, basic, formally verified UART controller