Formal Spec for RISC V

Skip to first unread message

Amr Zaky

Dec 26, 2022, 11:37:36 PM12/26/22

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?

--Amr Zaky

Tommy Murphy

Dec 27, 2022, 5:21:39 AM12/27/22
to Amr Zaky, RISC-V ISA Dev
There's SAIL in case that's of any use/interest to you?

Rishiyur Nikhil

Dec 27, 2022, 8:03:21 AM12/27/22
to Tommy Murphy, Amr Zaky, RISC-V ISA Dev
Yes, there is a formal spec for the Unprivileged RV32/64 IMAFDC and Privileged RISC-V ISAs.

The spec can be found at:

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

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''
    R.S.Nikhil, RISC-V Summit 2019.

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,


On Tue, Dec 27, 2022 at 5:21 AM Tommy Murphy <> wrote:
There's SAIL in case that's of any use/interest to you?

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
To view this discussion on the web visit
Reply all
Reply to author
0 new messages