You can add location information to your Tweets, such as your city or precise location, from the web and via third-party applications. You always have the option to delete your Tweet location history. Learn more
"A Bug-Free RISC-V Core without Simulation" by @tom_verbeure https://tomverbeure.github.io/risc-v/2018/11/19/A-Bug-Free-RISC-V-Core-without-Simulation.html …. Great article on riscv-formal. (And on how bad PicoRV32 is. Most of the criticism is justified. :)
This, however, isn't true. PicoRV32 marks all instruction fetches exactly so that it is possible to split the memory interface into separate instruction and data busses for users that want that. </Nitpick>pic.twitter.com/t72b3IOKiV
Perhaps he means that you cannot simultaneously fetch an instruction and perform a data load/store in the same cycle?
PicoRV32 takes at least three cycles for each instruction. You couldn't do that anyways, even if it had two memory interfaces.
It's possible yes, thanks to that signal. But it still adds some muxes as overhead internally to combine them and externally to separate them again
PicoRV32 does not have two memory load units that are "combined internally". It's just one state machine that performs one memory op at a time.
I have question. What does “without simulation” mean in the context of testing the core? The author mentions using riscv-formal before “simulation”. Presumably they mean “FPGA simulation”? i.e. RTL without tech mapping to FPGA i.e. synthesis? riscv-formal is in verilog?
They mean Verilog simulation.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
