Our great sponsors
-
-
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
-
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.
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.
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