Lessons learned while formally verifying the ZipCPU

on YouTube ↗26m

" summary

ZipCPU gets fully proven with SymbiYosys using induction and bounded checks, finding bugs tests never caught: bus reads that don’t halt, compressed-instruction edge cases, debug-port write ordering, and a multiply/divide race. Verification uses an abstract multiply to model behavior, aggregation forces a swap assumptions and assertions step across submodules, and many proofs finish from tiny counterexamples — one full-CPU proof needs only 18 clock cycles. End result still requires simulation; overall setup takes weeks, per-run proofs minutes.

AI-written summary · about

" chapters (22)

1. 0:00Intro
2. 1:59Formal verification properties
3. 4:51Prior formal verification
4. 5:48Pipeline stages
5. 6:18Execution units
6. 6:48Conditional execution
7. 8:00instruction cache
8. 9:08valid trace
9. 9:52data cache
10. 10:28formal methods
11. 11:20first lesson learned
12. 12:16debug port
13. 13:06pipeline
14. 13:33abstraction
15. 15:06aggregation
16. 15:39assumptions and assertions
17. 16:30multipass verification
18. 16:54assumptions
19. 17:08what happened
20. 17:49what I found
21. 19:33formal
22. 19:58Questions

" related talks

• 16mIntroduction to RISC-V Processor VerificationLarry Lapides · embedded world 2023
• 13mEarly RISC-V Software Verification with SIM-VLukas Jünger · embedded world 2023
• 13mOpen Source Formal Verification in VHDLPepijn de Vos · ORConf 2019
• 13mIntroduction to RISC-V Processor VerificationLarry Lapides · embedded world 2022
• 21mThe New Verification Ecosystem that Supports RISC-V Verification fo...Lee Moore, John Sotiropoulos · RISC-V Summit 2022
• 01h 12mPoster / Demo PreviewsJie Chen, Juan Fumero, Ekaterina Berezina, Wei Song, Chris Jones, Alberto Dassatti, Alex Bradbury, Mauro Olivieri, Zdenek Prikryl, Mary Bennett, Vasily Varaksin, Luke Kenneth Casson Leighton, Luca Carloni, Alexander Kamkin, Andrei Tatarnikov, Derek Atkins, Andrey Smolyarov, Christian Palmiero, Matt Cockrell, Christian Fabre, Nicolas Gaude, Hai Yu, Felix Kaiser, Heng Lin, Maja Malenko, Eric Matthews, Lesley Shannon, Paulo Matos, Lucas Morais, Aleksandar Pajkanovic, Matheus Ogleari, Shubhodeep Roy, Boris Shingarov, Christoph Schulz, Rui Hou, Dan Meng, Greg Sullivan, Robert Trout, Danny Ybarra · 8th RISC-V Workshop Barcelona 2018
• 17mPoster/Demo PreviewsAtish Patra, Kevin McDermott, Shubhodeep Roy Choudhury, Gajinder Panesar, Andrea Bocco, Tiago Trevian Jost · RISC-V Workshop Chennai 2018
• 21mA Comparative Analysis of RISC-V Architecture Based on the RISC-V SoC DV ExperienceMoonki Jang · RISC-V Summit North America 2023