Formal Specification
summary
Formal RISC‑V semantics implemented as a configurable, monadic Haskell monadic spec that leaves low‑level ops (get/set reg, memory I/O) abstract so the same core can be specialized into concrete simulators, symbolic executors, or TLB‑aware models. Toolchain includes automatic translation into proof assistants (via a Haskell→proof‑assistant tool) and hardware checks with Clash model checking and refinement proofs using Kami‑style refinement. Demonstrations include extracted Coq proofs of a C‑like compiler correctness and a partial‑evaluation FPGA‑style simulator; nondeterminism and VM/TLB blowup remain practical challenges.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:17What do we mean by formal spec?
- 2:45Hopes for our formal spec
- 11:27From parametrization to non-determinism 3/3
- 15:03Overall architecture of riscv-semantics
- 17:26Decode
- 21:13Executel in Cog
- 23:26An other benefits of being in a proof assistant
- 25:05Instrumenting the spec as a circuit
- 27:24Some fun with this spec
- 29:05Future work
related talks
24mStrong Formal Verification For RISC V: From Instruction Set Manual To RTL
32mFormal Specification of the RISC-V Instruction Set Architecture
02h 49mA Tour of the RISC V ISA Formal Specification
17mDemo: RISC-V Models for Verification, Software Development and Architectural Explor...
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
36mFlexible Instruction-Set Semantics via Abstract Monads
12mISA Formal Task Group Update
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...