ISA Formal Task Group Update
summary
A machine-readable formal ISA specification is written in a simple functional notation using a Haskell syntax subset, with an algebraic AST, a 32-bit decode, execute clauses for each opcode and a small interpreter for single-threaded semantics. Four months of weekly work cover RV32I RV64I M privileged subsets, a parser to connect to verification tools, and examples that expose real bugs (CSR retire-count ambiguity). Next targets: privilege coverage to enable booting Linux and adding concurrency/memory-model glue.
AI-written summary · about
chapters (7)
- 0:00Introduction and group overview
- 0:41Why formal specs matter
- 3:05Formal spec requirements and goals
- 6:44Choosing Haskell for the spec
- 8:10Spec excerpts and readability
- 10:23Why not use existing ISS as spec
- 10:44Current progress and next steps
related talks
32mFormal Specification of the RISC-V Instruction Set Architecture
02h 49mA Tour of the RISC V ISA Formal Specification
31mFormal Specification
38mBASE ISA
16mThe Morello ISA semantics, proof, and test generation
14mScaling Instruction-Selection Verification against Authoritative ISA Semantics
36mTowards a Formally-verified Software Toolchain for open ISAs
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures