Towards a Formally-verified Software Toolchain for open ISAs

on YouTube ↗36m

" summary

An open-source pipeline takes Sail PDL ISA models and drives a symbolic execution engine plus Z3 SMT solver and logic-program rewrite tools to synthesize assembler/encoding fragments and prove that a short POWER instruction sequence preserves a universal final-state invariant. It demonstrates automatic extraction of semantics from Sail, generates bitvector ASTs for the jit/OMR code cache, and finds no counterexample for straight-line code; loops and halting limits still block full program verification. Works reliably on Power and RISC‑V, limited for ARM/MIPS.

AI-written summary · about

" chapters (10)

1. 0:00Introduction and motivation
2. 2:11Testing vs formal verification
3. 5:02Why formal verification matters now
4. 8:17Symbolic CPU concept
5. 12:01Toolchain synthesis approach
6. 15:15Challenges with semantics
7. 20:16Acc Gen and Prologue
8. 23:12SAIL language for ISAs
9. 25:20Current toolchain system
10. 26:49Q&A on formal specs

" related talks

• 09mSemi-Automated Translation of a Formal ISA Specification to HardwareJonathan Balkind, Ben Hardekopf, Zachary D. Sisco, Timothy Sherwood, Harlan Kringen · PLARCH 2023
• 26mArchSem: Reusable Rigorous Semantics of Relaxed ArchitecturesPeter Sewell, Zongyuan Liu, Thibaut Pérami, Thomas Bauereiss, Brian Campbell, Nils Lauermann, Alasdair Armstrong · POPL 2026
• 02h 49mA Tour of the RISC V ISA Formal SpecificationRishiyur Nikhil · RISC-V Summit 2019
• 59mTutorial: High Level Sail OverviewBill McSpadden · RISC-V Summit 2022
• 20mSail RISC-V: Status and Future ChallengesAlasdair Armstrong · RISC-V Summit North America 2024
• 09mDemo: RISC-V Instruction Information Parsing and Storage for SAILPaul Clarke · RISC-V Summit North America 2023
• 09mBreaking the RISC-V Processor Customization Barrier with Formal VerificationSven Beyer · RISC-V Summit Europe 2024
• 16mAutomatic Test Generation and Verification for RISC-V Vector ExtensionXi Wang, Shenwei Hu · RISC-V Summit 2022