autofpga
A utility for Composing FPGA designs from Peripherals (by ZipCPU)
riscv-formal
RISC-V Formal Verification Framework (by SymbioticEDA)
autofpga | riscv-formal | |
---|---|---|
9 | 10 | |
156 | 550 | |
- | 3.6% | |
4.3 | 0.0 | |
4 months ago | about 2 years ago | |
C++ | Verilog | |
GNU General Public License v3.0 only | 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.
autofpga
Posts with mentions or reviews of autofpga.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2022-06-28.
-
How do you wire modules together?
I use AutoFPGA for connecting my top level components together. It handles bus composition and address assignment for me, while also creating linker, C header and Verilator simulation files for the project. Once a project is set up, reconfiguration is as easy as adding a file to the command line to add a component, or removing a file from the command line to remove a component. Make handles the rest.
-
Tricks to make AXI wiring faster in Verilog?
I use AutoFPGA for all my bus connections. A single @$(SLAVE.PORTLIST) or @$(SLAVE.ANSPORTLIST) automatically expands into the connections required when instantiating a module. It'll also instantiate the crossbar for you as well.
-
AXI InterConnect
Yes, I have posted an open source AXI interconnect. Unlike Xilinx's interconnect, mine doesn't automatically bridge between one bus width or clock and another, although some bridges exist in the same repository. Bridges exist, for example, for crossing clock domains, going from AXI3 to AXI4, from AXI4 to AXI4-lite, from AXI4 to a smaller AXI4-lite, and from AXI4-lite to a wider width. It's been enough to keep me from needing my own AXI4 interconnect, although AXI can be a real pain to wire up. As a result, I tend to use AutoFPGA for that purpose.
-
Hey Xilinx users, let me have it...
Now, whether or not AutoFPGA fits the bill for anyone--that's an entirely different question. I suspect the answer is, "No", but that's really a different conversation for a different time/thread. One of the things it can do is compose an AXI bus from multiple master and slave configurations--all using user controlled and very version controllable configuration files. The big problem it has (currently) is the lack of a strong verification suite. That's probably going to hit the top of my to-do list soon enough.
-
SoC FPGA design to ASIC
An SoC composer? You'll need something that takes multiple bus components and stitches them together. I've used AutoFPGA extensively for this purpose, and continue to do so today. It's biggest problem? I haven't put a lot of energy into marketing it, so the documentation is more lacking than I would like. Still, it's worked quite well for me and my intermediate tutorial (work in progress) provides some discussion of how to work with it.
-
Tricks to make AXI wiring faster in Verilog
AutoFPGA can do simple bus line pattern substitution. For example, these two configuration lines then expand to these 65 lines.
-
CPU DESIGN
There are also open source versions of many of the pieces you will need. I now use an open source crossbar interconnect for most of my designs. I use AutoFPGA to connect all the pieces together. I mentioned my flash controller above, but I also have a SD Card controller I've used quite successfully. I've also posted a UART to Wishbone bridge and discussed network debugging, both of which I use routinely with the ZipCPU. If for no other reason, these components allow me to load or update software on my CPU even after it's been placed into an FPGA. Of course, many of those components are tied to a Wishbone bus infrastructure. You may find you need a bridge of some type to connect different buses structures together--memory naturally tends to operate at one width and clock, video at another, and your CPU at another, so it helps at times to have a universal bus adapter kit handy.
-
Auto generate header files
I generated my own solution to this problem, a solution which I called AutoFPGA. It's not IP-XACT. It configures a design based upon a bus with (potentially) multiple masters and slaves. Configuration files are designed on a per-unit basis, with the intention that a slave (or master) configuration file could be removed to remove that portion of the design from the whole.
-
FPGA and Simulation tools for Risc-V design
If you wish to build a SOC design, you'll need some approach to assembling the bus together. There will be a lot of wires to connect, and a lot of logic to build just to get you off the ground. You'll find several SOC based building tools out there to use. I've built my own, AutoFPGA, which I use for assembling peripherals around a CPU based design. You might find an open source crossbar interconnect to be quite valuable as well. I've built crossbars for AXI, AXI-lite, and Wishbone (pipeline). I know there's a good Wishbone classic crossbar out there as well, I just don't have the link at my fingertips. (Good? It'll slow down your overall clock speed, while yielding poorer performance compared to Wishbone pipeline--but that's just the reality of working with Wishbone classic.)
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 autofpga and riscv-formal you can also consider the following projects:
verilog-axi - Verilog AXI components for FPGA implementation
riscv-arch-test
lion - Where Lions Roam: RISC-V on the VELDT
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.
rp32 - RISC-V processor with CPI=1 (every single instruction executed in a single clock cycle).
Rudi-RV32I - A rudimental RISCV CPU supporting RV32I instructions, in VHDL
riscv-tests
wb2axip - Bus bridges and other odds and ends
Cores-VeeR-EH1 - VeeR EH1 core
openarty - An Open Source configuration of the Arty platform