riscv-tests VS riscv-formal

Fully compliant to RISC-V how? Is it conforming to a specific RVI profile? The project states "By emulating a complete rv32i instruction set inside the wiring system of Terraria, we push back speeds to the early 70s era, tossing the ball firmly back into the court of silicon engineer without losing any software functionality."

So this is building a RISC-V *microcontroller* but what version of the ISA? 2.2 from 2017? Is it sucessfully passing conformance tests (https://github.com/riscv-software-src/riscv-tests)? I don't want to dunk on the project, but the title is over-selling and not scoping the context of the work. I look forward to some more updates from @misprit7!

Note: I'm the working group lead for distro-integration within the RISC-V Software Ecosystem (RISE) group.

Always test each of your changes on a battery of tests, like the riscv-tests. Have a way to generate a commit log of instructions and write back values and compare against an ISA simulator like spike or https://github.com/chipsalliance/dromajo.

You might be able to hook up your simulator to risc v-formal https://github.com/SymbioticEDA/riscv-formal

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.

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

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.

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.