riscv-formal
VexRiscv
riscv-formal | VexRiscv | |
---|---|---|
10 | 21 | |
550 | 2,277 | |
3.6% | 2.8% | |
0.0 | 7.3 | |
about 2 years ago | about 1 month ago | |
Verilog | Assembly | |
ISC License | MIT License |
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
-
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.
VexRiscv
-
Need help to build a RISC-V Processor on Artix-7 FPGA: Final Year Engineering Project Guide
With LiteX you can synthesize a VexRiscV processor. You can run Linux on it. The toolchain is pretty easy to use, as long as you use Xilinx Vivado to compile to gateware.
- RISC-V with AXI Peripheral
-
Intel discontinues Nios II IP
I don't get what's going on with licensing and device support. I'm missing something here perhaps, but we use Cyclone 10 GX onwards and Quartus Pro so I don't have enough context maybe. Have you considered swapping your Nios ii to a VexRISCV as a side note? At ~1 Dhrystone MIPS/MHz it's roughly double that of the Nios V, for very few resources. All open source too. None of the migration documentation support though, so I can't judge how hard it would be.
-
How Much Would It Cost For A Truly Open Source RISC-V SOC?
If you use LiteX to generate a VexRiscV system-on-a-chip, you can include an open source DDR DRAM PHY. This works on Xilinx Spartan-6, Spartan7Artix7/Kintex7/Virtex7 FPGAs, and Lattice ECP5 FPGAs. DDR/LPDDR/DDR2/DDR3 depending on the FPGA.
-
Which FPGA for getting into RISC-V?
Something like https://github.com/SpinalHDL/VexRiscv will take far fewer
-
Faster CRC32-C on x86
A CPU built around the Gentoo philosophy would look like https://github.com/SpinalHDL/VexRiscv ;). Don't want an MMU? Fine. Need a larger RAM interface? You got it. Barrel ALU for DSP? Sure.
Interpreted languages work by consolidating all of the optimization effort in the interpreter. This is similar to how CPUs work now, instead of extremely specific optimizations that are hard to create distributed among all code we use very general optimizations that push the limits of mathematics that is centralized in a CPU.
-----
Itanium had a lot of contemporary issues that made it not work. I would certainly blame Intel's business practices and reputation for a large part of it. There are likely niches for such processors. The VLIW is useful for DSP or graphics. Indeed, the only extant VLIW (that I know of) processor is the Russian Elbrus. I think the VLIW is only included to let them reuse a lot of the core logic of the CPU to drive a DSP engine, useful for radar and scientific simulation, though the sci sim would probably use commercial hardware which would be faster.
It works on GPUs because they're doing DSP, basically. We could have weirder topologies for GPUs however, like a massive string of ALUs driven off an embedded core, so you try to kachunk all your data in a single clock domain after configuring the ALU string.
-
Looking for a suitable open-source RISC-V for an embedded project
4) https://github.com/SpinalHDL/VexRiscv
-
What do think of Chisel HDL? is it worth learning over Verilog/SystemVerilog?
I really like Chisel HDL or any other new HDL languages like SpinalHDL or migen b/c it allows you to create some very complex yet modular designs. See VexRiscv or LiteX for instance. Languages like this exist b/c there is a need for it, but I wouldn't say that you should learn these new languages over verilog. All these languages output verilog/VHDL for now, but there is work being to done eliminate the need for outputting verilog; eventually, Chisel will output an open source CIRCT IR. Hope is to get EDA vendors to support this IR which I'm sure will take a while. For now, you should definitely learn Verilog or VHDL before Chisel.
- Looking for help with RISC-V softcore and VHDL
-
Thermal sensor mlx90640 with Nexys 3 fpga
I'd recommend giving vexriscv a look. It'll handily fit on your FPGA, leaving plants of room for I2C, VGA output, and whatever multiplication you end up wanting to do. It's very easy to get set up, and their example "briey" SOC even has VGA output already, but not hardware I2C (though you could easily bitbang it with the core). Adding in I2C via a "plugin" should be trivial.
What are some alternatives?
riscv-arch-test
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.
lion - Where Lions Roam: RISC-V on the VELDT
ibex - Ibex is a small 32 bit RISC-V CPU core, previously known as zero-riscy.
rp32 - RISC-V processor with CPI=1 (every single instruction executed in a single clock cycle).
RISCV-FiveStage - Marginally better than redstone
riscv-tests
wb2axip - Bus bridges and other odds and ends
Cores-VeeR-EH1 - VeeR EH1 core
darkriscv - opensouce RISC-V cpu core implemented in Verilog from scratch in one night!
autofpga - A utility for Composing FPGA designs from Peripherals