Formal Specification of the RISC-V Instruction Set Architecture

on YouTube ↗32m

" summary

An executable, machine‑readable RISC‑V ISA is implemented as an elementary Haskell executable spec that defines one‑instruction‑at‑a‑time semantics with explicit decoding, legality checks, and state transforms. The core is side‑effect free and uses pure functional core with IO wrappers to model memory and devices. A working wrapper boots Linux in Haskell (~5–6 min); aim is to become the compliance golden model and later extend to concurrent/multi‑core and weak memory semantics.

AI-written summary · about

" chapters (14)

1. 0:00Intro
2. 0:55Context
3. 5:56Challenges
4. 7:47Extensibility
5. 8:35Concurrency Weak Memory Models
6. 11:42Formal
7. 13:14Forbus
8. 13:52Design Principles
9. 16:43GL Instruction
10. 20:49Hidden Subtlety
11. 23:42Status Plans
12. 24:12Milestones
13. 24:56Enhancements
14. 25:56Questions

" related talks

• 02h 49mA Tour of the RISC V ISA Formal SpecificationRishiyur Nikhil · RISC-V Summit 2019
• 31mFormal SpecificationThomas Bourgeat · 8th RISC-V Workshop Barcelona 2018
• 12mISA Formal Task Group UpdateRishiyur Nikhil · 7th RISC-V Workshop 2017
• 24mStrong Formal Verification For RISC V: From Instruction Set Manual To RTLAdam Chlipala · 7th RISC-V Workshop 2017
• 36mAccelerate RISC-V Instruction Set Simulation by Tiered JIT CompilationYen-Fu Chen, Ching-Chun (Jim) Huang, Meng-Hung Chen, Chia-Heng Tu · VMIL 2024
• 19mRISC V ISA & Foundation OverviewRick O'Conner · 8th RISC-V Workshop Barcelona 2018
• 17mDemo: RISC-V Models for Verification, Software Development and Architectural Explor...Larry Lapides · RISC-V Summit 2022
• 36mFlexible Instruction-Set Semantics via Abstract MonadsAdam Chlipala, Thomas Bourgeat, Andres Erbsen, Samuel Gruetter, Ian J Clester, Pratap Singh, Andy Wright · ICFP 2023