Bill McSpadden

RIght. Does such a prover exist? I certainly have no desire to do directed random testing; I've left that world. If such a prover does exist (specifically for the RISCV...

The LLVM experimental switches that are used for this sort of thing are (per email with Philipp Tomsich): See [LINK](https://llvm.org/docs/RISCVUsage.html#experimental-extensions) for details. Short summary: -menable-experimental-extensions + "experimental-" (in the march=...

Hi Tim. Good question, and one that is being worked on. As you pointed out, the current method for configuring the model with command line switches is limited. Another option...

WARL CSRs are indeed a pain. And I've been using them as the pathological (ie - most difficult) case for configuration development. I think there are solutions to the problem....

Hi Mikhail. Is there a reason you are using the OCAML emulator rather than the C emulator? Most people are using the C emulator. For me to help debug this,...

Jessica wrote: "There are ambitions to overhaul the extension enabling..." Yes there are, driven mostly by me. (I intend to make use of the RISCV-Config YAML structures to configure the...

I was able to recreate this after some difficulty. I see the problem with Sail version 0.15, not 0.14. **(

I've assigned myself this issue. I'll be working on PRs for implementation of priv 1.13 features.

Something else that should be pointed out (for completeness sake)... Carl Friedrich Bolz-Tereick did some interesting work for improving the performance of Sail models using JIT techniques (See: https://drive.google.com/file/d/1DPftls6lgj6xCLC9n-siyb5sVkE_r3hl/view?usp=sharing )...

Yes, I’m in hospital right now and have limited ability to do much work. Martin Burger can also do a merge as well. The question for the team is: do...