REremexre·Nov 5, 2025
Test suites: https://github.com/riscv-software-src/riscv-tests
Formal model: https://github.com/riscv/sail-riscv
In RISC-V takes first step toward international ISO/IEC standardizationriscv
sail-riscv
Sail2021–2025
riscv / sail-riscv
sail-riscv
Sail RISC-V model
7Distinct people
12Mentions
0Explicit recommenders
807GitHub stars
What to know before exploring
What it is
Sail RISC-V model
GitHub
Where it is used
No documented product use has been verified yet.
What people are saying
No recommendation phrase was found in the indexed comments.
No classified warning is attached to this page. Read the discussions before treating silence as approval.
Also in these discussions
No other repository is repeatedly linked in the same discussions.
This week on Hacker News
Nov 7–Nov 14 UTC · Direct repository links and separately labeled related project stories. Indexed through 11/14/2026, 5:04:57 PM UTC.
No direct repository links were found in the indexed HN discussions over the past seven days. Older discussions are available below.
Mentions over time
HN mentions by year12 dated mentions
Observed mentions: 2021-12-02 18:11:02 UTC to 2025-11-05 14:06:36 UTC.
Counts come from the repository’s dated source evidence. Index cutoff: 2026-11-02 08:16:59 UTC.
View mention counts and date ranges
| Period | Start (UTC) | End (exclusive, UTC) | Mentions | Submissions | Comments |
|---|---|---|---|---|---|
| 2021 | 2021-01-01 00:00:00 UTC | 2022-01-01 00:00:00 UTC | 1 | 0 | 1 |
| 2022 | 2022-01-01 00:00:00 UTC | 2023-01-01 00:00:00 UTC | 1 | 0 | 1 |
| 2023 | 2023-01-01 00:00:00 UTC | 2024-01-01 00:00:00 UTC | 5 | 0 | 5 |
| 2024 | 2024-01-01 00:00:00 UTC | 2025-01-01 00:00:00 UTC | 1 | 0 | 1 |
| 2025 | 2025-01-01 00:00:00 UTC | 2026-01-01 00:00:00 UTC | 4 | 1 | 3 |
What Hacker News says
12 sourcesAnother way to build emulators that I am very interested in is to start from a spec, and automatically translate it into executable code. High-fidelity emulators have a lot of potential for testing and verification.
The best example I know of is Sail [1]. Among other, they have RISC-V spec [2] and a bunch of compiler back-ends. They can already generate C or OCaml emulators, and I have been working on a new Rust back-end recently.
[1]: https://github.com/rems-project/sail
[2]: https://github.com/riscv/sail-riscv
In Writing a RISC-V Emulator in RustI've used this a lot via the RISC-V Sail model: https://github.com/riscv/sail-riscv
It's a really nice language - especially the lightweight dependent types. Basically it has dependent types for integers and bit-vector lengths so you can have some really nice guarantees. E.g. in this example https://github.com/Timmmm/sail_demo/blob/master/src/079_page...
we have this function type
val splitAccessWidths : forall 'w, 0 <= 'w . (xlenbits, int('w)) ->
{'w0 'w1, 'w0 >= 0 & 'w1 >= 0 & 'w0 + 'w1 == 'w . (int('w0), int('w1))}
Which basically means it returns a tuple of 2 integers, and they must sum to the input integer. The type system knows this. Then when we do this:
let (width0, width1) = splitAccessWidths(vaddr, width);
let val0 = mem_read_contiguous(paddr0, width0);
let val1 = mem_read_contiguous(paddr1, width1);
val1 @ val0
Read the rest
The type system knows that `length(val0) + length(val1) == width`. When you concatenate them (@ is bit-vector concatenation; wouldn't have been my choice but it's heavily OCaml-inspired), the type system knows `length(val1 @ val0) == width`.
If you make a mistake and do `val1 @ val1` for example you'll get a type error.
A simpler example is https://github.com/Timmmm/sail_demo/blob/master/src/070_fanc...
The type `val count_ones : forall 'n, 'n >= 0. (bits('n)) -> range(0, 'n)` means that it's generic over any length of bit vector and the return type is an integer from 0 to the length of the bit vector.
I added it to Godbolt (slightly old version though) so you can try it out there.
It's not a general purpose language so it's really only useful for modelling hardware.
Show HN: Miralis – a RISC-V virtual firmware monitor
Miralis is a RISC-V firmware that virtualizes RISC-V firmware. In other words, it runs firmware in user-space (M-mode software in U-mode).
The fact that this is even possible is interesting: indeed, not all ISAs are virtualizable, and the same applies for their firmware mode. It all boils down to the virtualization requirements [1], which is a great read if you haven't come across it yet. Arm's EL3 cannot be virtualized, for instance, because some instructions, such as `cpsid`, are sensitive but do not trap (`cpsid` is a nop in user-space).
If you have a VisionFive 2 or a HiFive Premier P550, you can try it out, the instructions are in the documentation [2, 3]. Of course, it runs on QEMU too.
As Miralis is a research project, we have also been using it as a vehicle to explore other research ideas, such as automated verification of hypervi
Read the rest
sors [4]. For instance, we verified instruction emulation by comparing Miralis' implementation with the reference RISC-V executable specification [5], which we translated to Rust.
It has been fun working on Miralis, I hope you'll find it interesting too!
[1]: https://dl.acm.org/doi/pdf/10.1145/361011.361073
[2]: https://miralis-firmware.github.io/docs/platforms/visionfive...
[3]: https://miralis-firmware.github.io/docs/platforms/premierp55...
[4]: https://charlycst.github.io/papers/lightweight-hypervisor-ve...
[5]: https://github.com/riscv/sail-riscv
I've been doing a lot of work with Sail (not SAIL btw) and I'm not sure I agree with the points about it.
There's already a way to extract functions into asciidoc as the author noted. I've used it. It works well.
The liquid types do take some getting used to but they aren't actually used in most of the code; mostly for utility function definitions like `zero_extend`. If you look at the definition for simple instructions they can be very readable and practically pseudocode:
https://github.com/riscv/sail-riscv/blob/0aae5bc7f57df4ebedd...
A lot of instructions are more complex or course but that's what you get if you want to precisely define them.
Overall Sail is a really fantastic language and the liquid types really help avoid bugs.
The biggest actual problems are:
1. The RISC-V spec is chock full of undefined / implementation defined beha
Read the rest
viour. How do you capture that in code, where basically everything is defined. The biggest example is probably WARL fields which can do basically anything. Another example is decomposing misaligned accesses. You can decompose them into any number of atomic memory operations and do them in any order. E.g. Spike decomposes them into single byte accesses. (This problem isn't really unique to Sail tbf).
2. The RISC-V Sail model doesn't do a good job of letting you configure it currently. E.g. you can't even set the spec version at the moment. This is just an engineering problem though. We're hoping to fix it one day using riscv-config which is a YAML file that's supposed to specify all the configurable behaviour about a RISC-V chip.
I definitely agree about the often wooly language in the spec though. It doesn't even use RFC-style MUST/SHOULD/MAY terms.
The official formal specification of the Vector Extension has just been merged into the Golden RISC-V model:
https://github.com/riscv/sail-riscv/commit/c90cf2e6eff5fa4ef...
I expect that this will help stabilise compiler support and facilitate other RISC-V extensions, like RISC-V Vector Crypto, also to progress.
In RISC-V Vector benchmark resultsInteresting. Difficult to tell how complex the bugs are though. Some of them seem to be just triggered by accessing non-existent CSRs which suggests those chips haven't been very well verified already?
Also:
> Cascade discovered
3 inaccurate performance counter bugs (Perfcnts) in Kronos,
VexRiscv and BOOM (K4, V13, B2). They incur an offset in
the retired instruction counters when written by software.
Funnily enough the Sail model had this bug too! https://github.com/riscv/sail-riscv/issues/256
In Cascade: CPU fuzzing via intricate program generation> loose specification of the RISC-V ISA.
This is being worked on with the Sail model [1]. In order for a RISC-V extension to be ratified it ought to be implemented in Sail. The understanding is also that the RISC-V ISA manual should be built with code snippets from the Sail model (similar to how the Arm ARM is build from ASL definition). The main issue is a lack of people willing and able to write Sail for RISC-V. But that is beginning to change, since RISC-V member companies are increasingly use Sail. As an example, the RISC-V exception type is defined in [2]. Is that precise enough for you?
The formal RISC-V ISA specification is not finished, you are welcome to make a PR to clarify things.
[1] https://github.com/riscv/sail-riscv
[2] https://github.com/riscv/sail-riscv/blob/master/model/riscv_...
In Arm’s Cortex A510: Two Kids in a Trench Coat>it allows to formally verify the correctness of a particular ISA
That must be hypothetical. "Functionalness" of the language/code doesn't make everything that is written automatically subject to formal verification. (mechanized or pen and paper). What kind of correctness properties does it actually allow to formally verify? I understand if it was the F* language, which is a full blown dependently typed proof checker, but with F#, which is defined by the implementation and 300 page English spec, I don't think you can verify anything interesting. As far as I know F# itself doesn't have mechanized formal semantics and its type system could be unsound.
https://github.com/mit-plv/riscv-coq and https://github.com/riscv/sail-riscv (don't know how complete they are) approaches actually allow to formally (mechanically) verify riscv properties.
Yo
Read the rest
ur executable specification could probably be called "Formal", in the same sense as a PDF spec being called "Formal", but being subject to verification by the virtue of F# being functional or being written in the functional style might be pushing it too far.
Basically yes, but with the goal being semantic correctness rather than performance.
Seems to be similar to the official Sail model but F# instead of Sail.
Kind of funny since Sail can already compile to OCaml - probably wouldn't be too hard to add a F# backend. Then again, more independent implementations are always nice to have.
Would be interesting to know their motivation for this.
Edit: actually this looks like it has been dead for 3 years so maybe it was just a precursor to the Sail model.
https://github.com/riscv/sail-riscv
In F# RISC-V Instruction Set formal specificationNice work!
How did you debug it? Did you run it against the 'official' RISC-V models Spike [1] or Sail [2]?
[1] https://github.com/riscv-software-src/riscv-isa-sim
[2] https://github.com/riscv/sail-riscv
In Show HN: Libriscv – RISC-V userspace emulator libraryIt's best to think of RISCV not as a single ISA (= instruction set architecture), but a parametric ISA. The extensions are parameters.
RISCV offers lots of official extensions to choose from, such as M, A, F, D, P, V, ....
In addition you have the 32 vs 64 bit data width parameter. Any specific ISA will have to instantiate those parameters, like e.g. so: RISCV32MFP
or
RISCV64MAF.
Any implementation of e.g. RISCV64MAF will have to implement in silicon exactly those assembly command (and supporting features) that the M, A and F extension demand, with 64 bit register width.
Like in OO-programming the class constructors take arguments that parameterise the created object.
------
Regarding an implementation, given that RISCV is an ISA, not an ISA implementation, you need to provide a functional model. The official standard is [1] but
Read the rest
it's a bit behind the ratified extensions. For example [2] defines the (ISA-visible)
registers, while [3] gives you the instruction decoding and execution clause for the most base instruction set. [4] describes part of one of the available address translation modes (for the 32 bit variant of the ISA). Note: in modern processors page-table walks are hardware accelerated, so OS and processor need to use the same format here, which is why this is part of the ISA.
[1] https://github.com/riscv/sail-riscv/tree/master/model
[2] https://github.com/riscv/sail-riscv/blob/master/model/riscv_...
[3] https://github.com/riscv/sail-riscv/blob/master/model/riscv_...
[4] https://github.com/riscv/sail-riscv/blob/master/model/riscv_...