Democratising Formal Verification of RISC V Processors

on YouTube ↗24m

" summary

A vendor‑agnostic proof kit compiles a RISC‑V core into SystemVerilog assertions and runs on Jasper Cadence Synopsys and OneSpin, requiring ~15–20 lines of setup to map signals. The workflow proves ~80% of properties in ~2 hours with LSU checks taking ~24 hours, and produces exhaustive, 100% determined proofs. Results include 70 million properties with ~900 helpers, a debug timing bug that corrupts almost every instruction in one core, a load overwrite bug in another, and found 8 serious violations in lockstep checks.

AI-written summary · about

" chapters (10)

1. 0:00Introduction
2. 2:32How are we driving changes
3. 3:08Formal verification of big designs
4. 3:48Formal verification of 5 designs
5. 6:25Architectural and micro architectural issues
6. 7:10RISCV 5C and Ibex
7. 9:49Follow a flow
8. 14:05XM is Risk
9. 15:44Ibex is Risk
10. 18:12Ibex Microarchitecture

" related talks

• 28mFormal Assurance for RISC-V ImplementationsDaniel Zimmerman, Joseph Kiniry · 8th RISC-V Workshop Barcelona 2018
• 25mRISC-V System-level Certification from Verification FoundationsAdnan Hamid · RISC-V Summit North America 2025
• 10mDemo: Open Standards and Verification Methodology for RISC-V ProcessorsAimee Sutton · RISC-V Summit North America 2023
• 12mHardware Verification of Timing Side Channel Freedom in the Spectre EraAdam Chlipala, Clément Pit-Claudel, Thomas Bourgeat, Stella Lau · PLARCH 2023
• 16mAutomated Certification and Benchmarking for RISC-V ArchitecturesEnrique Pallares · RISC-V Summit North America 2025
• 45mVerified seL4 on secure RISC-V processorsGernot Heiser · linux.conf.au 2020
• 19mOpen-Source Commercial-Grade RISC-V IOMMU with VerificationManuel Sánchez Rodríguez, Saad Waheed · RISC-V Summit North America 2024
• 18mProving RISC-V Security Model Compliance with SESIPEve Atallah · RISC-V Summit 2022