The RISC-V Formal Specification Technical Group: Progress Report
summary
Working group of about 10–15 regular members produces a machine-readable ISA semantics implemented in Haskell (MIT variant) that runs ELF/memory images as an executable simulator and is already used for tandem verification by comparing per-instruction state-change packets against implementations. Toolchain links include Clash/Verilog generation and model checking against Spike; a proof‑assistant connector supports small compiler proofs. Current scope is a complete sequential semantics (FP largely deferred); a spec release is targeted in ~two months, with later integration of the weak memory model.
AI-written summary · about
chapters (6)
related talks
27mRISC-V BoF
17mDemo: RISC-V Models for Verification, Software Development and Architectural Explor...
13mEarly RISC-V Software Verification with SIM-V
10mEnabling Production Program Software Development for RISC-V
21mRISC-V ISA & Foundation Overview
15mRISC-V Foundation Presentation
21mA Comparative Analysis of RISC-V Architecture Based on the RISC-V SoC DV Experience
19mFormal Methods for Hardware Software Integration on RISC V Embedded Systems