Strong Formal Verification For RISC V: From Instruction Set Manual To RTL

on YouTube ↗24m

" summary

Claims a full machine-checked refinement from the RISC‑V ISA to RTL using a Coq proof assistant guided framework and a Bluespec-like language that compiles to RTL with a formally verified compiler planned. Delivers two implemented RISC‑V cores so far: a 32‑bit microcontroller-class core proved correct, and a 64‑bit desktop-class core in progress that can run a Linux boot prefix against the formal spec. Proves a two‑level cache coherent memory for any number and size of caches and composes component proofs into system‑level guarantees.

AI-written summary · about

" chapters (10)

1. 0:00Intro
2. 0:59A Cartoon View of Digital Hardware Design
3. 3:13Analyze Isolated Components
4. 4:08Start Over For Each Design
5. 6:03The Big Ideas (from Bluespec)
6. 10:08Some Example Kami Code (simple FIFO)
7. 11:11An Example Kami Proof (pipelined processor)
8. 15:46Some Useful Refinement Tactics
9. 17:50Key Ingredient
10. 20:54The Promise of this Approach

" related talks

• 31mFormal SpecificationThomas Bourgeat · 8th RISC-V Workshop Barcelona 2018
• 18mRISC-V Spotlight: Improving RISC-V Quality with Verification Standards and Advanc...Simon Davidmann · RISC-V Summit 2022
• 17mDemo: RISC-V Models for Verification, Software Development and Architectural Explor...Larry Lapides · RISC-V Summit 2022
• 02h 49mA Tour of the RISC V ISA Formal SpecificationRishiyur Nikhil · RISC-V Summit 2019
• 09mBreaking the RISC-V Processor Customization Barrier with Formal VerificationSven Beyer · RISC-V Summit Europe 2024
• 32mFormal Specification of the RISC-V Instruction Set ArchitectureRishiyur Nikhil, Niraj Sharma · RISC-V Workshop Chennai 2018
• 21mThe New Verification Ecosystem that Supports RISC-V Verification fo...Lee Moore, John Sotiropoulos · RISC-V Summit 2022
• 20mRISC V Software State of the UnionRandy Allen · RISC-V Summit 2019