3 ms·

I am excitedly awaiting the full release of ASL1 from Arm. I wonder if anyone with more knowledge might be able to comment on how it compares with Sail and/or w

I am excitedly awaiting the full release of ASL1 from Arm. I wonder if anyone with more knowledge might be able to comment on how it compares with Sail and/or when we might expect to see a full Arm specification in ASL1 (as opposed to the current spec which is normal ASL and appears to be incompatible with the upcoming version). Perhaps in the future there might also be a RISC-V specification written in ASL1.

Peter_Sewell 2y ago
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 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/built/sail_to_asciidoc.pdf 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/release/riscv-spec-sail-draft.pdf https://github.com/rems-project/riscv-isa-manual/blob/sail/r...).
adreid 2y ago
Note that herd contains an ASL1 implementation. https://github.com/herd/herdtools7/tree/master/asllib https://github.com/herd/herdtools7/tree/master/asllib

Peter_Sewell 2y ago

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 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/built/sail_to_asciidoc.pdf 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/release/riscv-spec-sail-draft.pdf https://github.com/rems-project/riscv-isa-manual/blob/sail/r...).

adreid 2y ago

Note that herd contains an ASL1 implementation. https://github.com/herd/herdtools7/tree/master/asllib https://github.com/herd/herdtools7/tree/master/asllib