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:
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 behaviour. 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.
I agree on the beauty of liquid types. I encourage HN to learn Sail, simply to get experience with liquid types. The Sail specification of RISCV is currently the only place where liquid types are used in industrial code. (There is Liquid Haskell and Liquid Rust, but they are research prototypes.) I expect that over the next decade or two, liquid types will come to the programming mainstream.
The configurability problem has several main parts.
(1) It's a Turing complete problem as the informal RISCV specification gives you so much freedom, including all those IMPDEFs. The specification of a complex, configurable ISA will always be intrinsically complex and syntax can only do so much about presenting this intrinsic complexity.
(2) Sail's lack of a clear, easy to use module system for configuration of the exact RISCV version to be emulated.
That's not really what I meant. It's very easy to configure which instructions or CSRs exist, and excluding custom extensions there are really only two options for behaviour, so you just have a flag `haveSomeExtension()` to enable the instructions and CSRs. The Sail model has some of these flags already.
If you write to a WARL field in a CSR the chip can use more or less any legalisation logic it wants. Configuring that is very difficult (though there is a decent attempt in riscv-config).
Yes I don't think Ssstrict is very complete. In fact while I was looking for it, I'm not sure it's been fully defined yet, beyond some postings on the tech-profiles list.
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 behaviour. 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.