Formal Spec for RISC V

[Amr Zaky]

Hi

Is there a formal RISC V spec? Something like ARM's ASL that can be directly executed or translated to some HW or SW language?

Thanks

--Amr Zaky

[Tommy Murphy]

There's SAIL in case that's of any use/interest to you?

https://github.com/riscv/sail-riscv

[Rishiyur Nikhil]

Yes, there is a formal spec for the Unprivileged RV32/64 IMAFDC and Privileged RISC-V ISAs.

The spec can be found at:

    https://github.com/riscv/sail-riscv



The spec is written in Sail, a language (DSL) for ISA formal
specifications from U.Cambridge, UK.  Sail website:

    https://github.com/rems-project/sail

The RISC-V formal spec can be compiled into a simulator for RISC-V,
which can be used as a golden reference model.  The executable is
capable of booting Linux in a few seconds.

A 2-year tour of the spec can be found at:

    ``A Tour of the RISC-V ISA Formal Specification''
    https://github.com/rsnikhil/RISCV_ISA_Spec_Tour
    R.S.Nikhil, RISC-V Summit 2019.
    Video: https://www.youtube.com/watch?v=k3NhEtk8TAs

There was another talk on the subject at the RISC-V Summit a few weeks
ago, for which you may find links on the RISC-V Summit web site:

    ``High Level Sail Overview'', by Bill McSpadden, RISC-V Summit 2022.

Best regards,

Nikhil
(nik...@bluespec.com)

On Tue, Dec 27, 2022 at 5:21 AM Tommy Murphy <tommy_...@hotmail.com> wrote:

There's SAIL in case that's of any use/interest to you?

https://github.com/riscv/sail-riscv

--
You received this message because you are subscribed to the Google Groups "RISC-V ISA Dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to isa-dev+u...@groups.riscv.org.
To view this discussion on the web visit https://groups.google.com/a/groups.riscv.org/d/msgid/isa-dev/LO0P265MB68667600622BE74C5A615CDDF9ED9%40LO0P265MB6866.GBRP265.PROD.OUTLOOK.COM.