Very first draft of abstract for presentation on riscv-formal for a few upcoming conferences. Constructive feedback requested.pic.twitter.com/50LmDMZ8Qp
-
Many of the PicoRV32 bugs where found using formal methods. But this was before riscv-formal.
Essentially I was comparing two differently configured versions of the core and/or different memory timings and checked >>
-
-
if the sequence of memory operations performed as function of the initial content of the memory is invariant between those versions.
-
There is still one known bug left from this, but it's a performance bug: In certain (rare) situations PicoRV32 fetches an instruction twice.
End of conversation
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.