sail VS riscv-isa-manual

Sail is pretty similar to ASL (both current ASL and ASL 1.0) except that (1) it has a more expressive type system, so that bitvector lengths can all be statically checked, (2) it has proper tagged unions and pattern matching, and (3) there's a wide range of open-source tooling available, for execution, specification coverage, generating emulators, integrating with relaxed concurrency models, generating theorem-prover definitions, etc. We've recently updated the Sail README, which spells some of this out: https://github.com/rems-project/sail .

As Alastair Reid says, one of the main things missing in the current RISC-V specification documents is simply that the associated Sail definitions are not yet interspersed with the prose instruction descriptions. The infrastructure to do that has been available for some time, in the Sail AsciiDoc support by Alasdair Armstrong (https://github.com/Alasdair/asciidoctor-sail/blob/master/doc...) and older LaTeX versions by Prashanth Mundkur and Alasdair (https://github.com/rems-project/riscv-isa-manual/blob/sail/r...).

That's completely feasible and there are languages that do this. It doesn't really eliminate the need to run your program unless the inputs to your program are also completely restricted types like One, Two, Three. In which case yeah, you don't need to run it and the type system can just tell you the answer.

I believe you can do that sort of thing in loads of type systems, e.g. Typescript, but there are languages that intentionally support it. I use a niche DSL that has fancy types like this called Sail. https://github.com/rems-project/sail

In my experience the downsides of these fancy "first class type systems" are

1. More incomprehensible error messages.

2. The type checker moves from a deterministic process that either succeeds or fails in an understandable way, to SMT solvers which can just say "yep it's ok" or "nope, couldn't prove it", semi-randomly, and there's little you can do about it.

Still my experience of Sail is that it's very comfortable to go a little bit further into SMT land, and my experience of Dafny is that it's very unpleasant to go full formal-verification at the moment.

I've done a fair bit of hardware formal verification too and that's a different story - very easy and very powerful. I'm hoping one day that software formal verification is like that.

https://github.com/riscv/riscv-isa-manual/releases

Regarding the recent "How to improve the RISC-V specification" post [0], I just wanted to point out, that the latest draft manual is already a great improvement. (see link above)

It includes a lot of the newly ratified extensions: bitmanip,zicond,vector,vector crypto, ...

And there are a bunch of included SAIL definitions for bitmanip and zicond, but other instructions are still missing the SAIL code. Most notably, the SAIL definitions from the RV32I/RV64I base isa are also missing.

I asked for the further SAIL integration plans here: https://github.com/riscv/riscv-isa-manual/issues/1369

Here is an example SAIL snippet from cpopw:

    let bitcount = 0;

I encourage you to look at the newest isa manual draft on github: https://github.com/riscv/riscv-isa-manual/releases

It includes the more recently extensions, and e.g. the bitmanip instructions all have associated pseudo code.

Here is e.g. the code for cpopw:

    let bitcount = 0;

I tried searching the spec [1] for "overflow" and here is what it says at page 17:

> We did not include special instruction-set support for overflow checks on integer arithmetic operations in the base instruction set, as many overflow checks can be cheaply implemented using RISC-V branches.

> For general signed addition, three additional instructions after the addition are required

Is this "cheap", replacing 1 instruction with four? According to some old mainframe era research (cannot find link now), addition is the most often used instruction and they suggest that we should replace each one with four?

Their "rationale" is not rational at all. It doesn't make sense.

Overflow check should be free (no additional instructions required), otherwise we will see the same story we have seen for last 50 years: compiler writers do not want to implement checks because they are expensive; language designers do not want to use proper arithmetic because it is expensive. As a result, there will be errors and vulnerabilities. A vicious circle.

[1] https://github.com/riscv/riscv-isa-manual/releases/download/...

Why not use the actual release PDF instead from their github? https://github.com/riscv/riscv-isa-manual

https://github.com/riscv/riscv-isa-manual/releases/download/Priv-v1.12/riscv-privileged-20211203.pdf Part 2

If you don't want to cheat then read the RISC-V ISA manual: https://github.com/riscv/riscv-isa-manual/releases/download/Ratified-IMAFDQC/riscv-spec-20191213.pdf

Yeah you are on the right track. Processors are designed on top of an Instruction Set Architecture (ISA). For an example you can look on top of the RISC-V specifications:https://github.com/riscv/riscv-isa-manual/releases/download/Ratified-IMAFDQC/riscv-spec-20191213.pdf (possible PDF download)