That's why you need to formal, and then formal your formal. https://github.com/ucb-bar/riscv-torture/issues/11 …pic.twitter.com/GPM5UYeKgb
-
With PicoRV32 it seems I found those problems all with the other formal methods I used before I started my work on riscv-formal.
Essentially comparing the behavior of two PicoRV32 cores (same or different config) on the same memory image but with different timings.
-
-
So all the problems that are left here are related to ISA compliance where PicoRV32 consistently was not conforming to the ISA spec.
-
But the next RISC-V CPU I'll target with riscv-formal is RISC-V Rocket. Big hopes that I'll find more interesting bugs there.
- Show replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.