A Tour of the RISC V ISA Formal Specification

on YouTube ↗02h 49m

" summary

The RISC‑V ISA is encoded in the Sail language as executable, strongly typed AST + encode/decode + execute + assembly clauses and the team produces OCaml/C simulators via Sail→C→emulator. The repo runs the standard validation harness including 229 standard ISA tests and a compliance suite across RV32/RV64 configurations. Floating point uses Berkeley SoftFloat for arithmetic. Extensions are added by scattering AST, encoder and execute clauses. The model runs and compares signatures and is already used to validate ARMv8 translations.

AI-written summary · about

" chapters (35)

1. 0:00Start
2. 2:42Objectives
3. 10:32What Is an Icy Formal Spec
4. 11:48Readability
5. 17:24Reading the Isis Spec
6. 19:31Execute Semantics of One Class of Instructions
7. 21:07Instruction Formats
8. 25:05Virtual Memory
9. 25:57Type Checking and Strong Types
10. 29:21Syntax
11. 34:34Reading from the Register
12. 36:28Effects Declaration
13. 51:11Right Function General Pattern
14. 51:49Output Type
15. 52:48Overloading
16. 55:49Data Structure
17. 1:00:55The Execute Function
18. 1:03:35Six Encoding Types for Instructions
19. 1:04:02Major Opcode
20. 1:11:58The Execute Clause
21. 1:16:35How Do You Know It's a Signed or Unsigned Addition
22. 1:25:37Assembly Mapping
23. 1:32:39Encode Decode Mapping
24. 1:34:56Execute Clause
25. 1:36:16Execute Clause
26. 1:37:43Handle Memory Exception
27. 1:39:28Load Instruction
28. 1:42:52Translate Address
29. 1:49:26handle mem exception
30. 1:49:51Exception Handler
31. 1:51:16Trap Handler
32. 1:56:03Sequential Fetch Execute Loop
33. 1:56:41Loop
34. 1:58:06Dispatch Interrupt at Current Privilege
35. 2:03:31What Made Us Choose the Sale Model

" related talks

• 20mSail RISC-V: Status and Future ChallengesAlasdair Armstrong · RISC-V Summit North America 2024
• 20mRISC-V Vector Sail Model and Test GenerationXi Wang, Yifei Zhu · RISC-V Forum: Vector & Machine Learning 2021
• 59mTutorial: High Level Sail OverviewBill McSpadden · RISC-V Summit 2022
• 09mDemo: RISC-V Instruction Information Parsing and Storage for SAILPaul Clarke · RISC-V Summit North America 2023
• 32mFormal Specification of the RISC-V Instruction Set ArchitectureRishiyur Nikhil, Niraj Sharma · RISC-V Workshop Chennai 2018
• 16mAutomatic Test Generation and Verification for RISC-V Vector ExtensionXi Wang, Shenwei Hu · RISC-V Summit 2022
• 26mArchSem: Reusable Rigorous Semantics of Relaxed ArchitecturesPeter Sewell, Zongyuan Liu, Thibaut Pérami, Thomas Bauereiss, Brian Campbell, Nils Lauermann, Alasdair Armstrong · POPL 2026
• 24mStrong Formal Verification For RISC V: From Instruction Set Manual To RTLAdam Chlipala · 7th RISC-V Workshop 2017