Hmm, thanks for keeping me honest; I took another look after reading your response and I've changed my mind a bit :)
I think my primary criticism is the way in which the formal specification is surfaced in RISC-V as opposed to ARM rather than any issue with Sail in particular.
In ARM, the relevant portions of the pseudocode/ASL are available directly in the architecture reference manual. A snippet is either included directly underneath the relevant instruction or there is a link to it. This makes it very easy to use since only the relevant bits are presented when it is being used for reference/human spec reading purposes. This relationship to pseudocode/ASL, of course, makes sense given the history of ASL. The documentation pseudocode was originally just a nice and clearer way to explain how instructions work (free from the trappings of natural language). Later, they cleaned up the pseudocode and created an actual language specification for it so that it could be used as a formal model.
In RISC-V, we don't really get any such luxuries. If you find yourself confused about how exactly an instruction works, you have to somehow know that the Sail model is the official specification (it is not called out anywhere in the natural language spec!) and then go trawl through the entire model yourself hunting for the definition of your instruction. This isn't super hard if you know what you're doing, but there is a lot of other machinery in these models that you can trip over (it includes instruction binary encoding formats and the assembler language specification as well). I would say that I'm comfortable using the model as a reference but it's definitely not as easy to access as it is over on ARM.
I see now though that there is an effort to integrate the Sail source into the natural language specification. I hope that makes it eventually, it'll be a big quality of life improvement.
I think my primary criticism is the way in which the formal specification is surfaced in RISC-V as opposed to ARM rather than any issue with Sail in particular.
In ARM, the relevant portions of the pseudocode/ASL are available directly in the architecture reference manual. A snippet is either included directly underneath the relevant instruction or there is a link to it. This makes it very easy to use since only the relevant bits are presented when it is being used for reference/human spec reading purposes. This relationship to pseudocode/ASL, of course, makes sense given the history of ASL. The documentation pseudocode was originally just a nice and clearer way to explain how instructions work (free from the trappings of natural language). Later, they cleaned up the pseudocode and created an actual language specification for it so that it could be used as a formal model.
In RISC-V, we don't really get any such luxuries. If you find yourself confused about how exactly an instruction works, you have to somehow know that the Sail model is the official specification (it is not called out anywhere in the natural language spec!) and then go trawl through the entire model yourself hunting for the definition of your instruction. This isn't super hard if you know what you're doing, but there is a lot of other machinery in these models that you can trip over (it includes instruction binary encoding formats and the assembler language specification as well). I would say that I'm comfortable using the model as a reference but it's definitely not as easy to access as it is over on ARM.
I see now though that there is an effort to integrate the Sail source into the natural language specification. I hope that makes it eventually, it'll be a big quality of life improvement.