Where Lions Roam: RISC-V on the VELDT

This page summarizes the projects mentioned and recommended in the original post on reddit.com/r/haskell

Our great sponsors
  • Scout APM - Less time debugging, more time building
  • SonarQube - Static code analysis for 29 languages.
  • SaaSHub - Software Alternatives and Reviews
  • lion

    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.

  • VexRiscv

    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.

  • Scout APM

    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.

  • riscv-formal

    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

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts