Where Lions Roam: RISC-V on the VELDT (by standardsemiconductor)
In addition, you can actually set the riscv-formal suite to verify correctness by k-induction: https://github.com/SymbioticEDA/riscv-formal/pull/28 https://symbiyosys.readthedocs.io/en/latest/quickstart.html#beyond-bounded-model-checks although I concur that by looking at https://github.com/standardsemiconductor/lion/blob/main/lion-formal/app/Main.hs the lion core is only verified with BMC.
A FPGA friendly 32 bit RISC-V CPU implementation
Sorry for the gobs of lack of knowledge in this question, but are RISC-V implementations generally interchangeable? The precursor handheld is currently based on a VecRiscv soft core, which the project describes as "100 MHz customized VexRISC-V RV32IMAC + MMU core with 4k caches". Would replacing VecRiscv with Lion be a huge project, or just swapping around some files? I haven't done anything FPGA since college, so I'm guessing this question just oozes confusion, but running a formally verified RiscV on the precursor sounds amazing to me.
Less time debugging, more time building. Scout APM allows you to find and fix performance issues with no hassle. Now with error monitoring and external services monitoring, Scout is a developer's best friend when it comes to application development.
RISC-V Formal Verification Framework
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
Show HN: Superscalar RISC-V CPU written in Clash
1 project | news.ycombinator.com | 23 Oct 2021
How to use a RISC V core for other purposes?
2 projects | reddit.com/r/RISCV | 8 Jun 2021
Show HN: A RISC-V core written in Racket
2 projects | news.ycombinator.com | 1 May 2021
Lion is a formally verified, 5-stage pipeline RISC-V core
1 project | reddit.com/r/RISCV | 4 Mar 2021
Lion: A formally verified, 5-stage pipeline RISC-V core
1 project | reddit.com/r/patient_hackernews | 4 Mar 2021