More than the Core Verifying RISC V SoCs

on YouTube ↗18m

" summary

OneSpin formalizes the RISC‑V ISA into SystemVerilog assertions and uses interval property checking to link pipeline behavior to a sequential instruction model. A semi‑automated app generates config‑specific assertions bound to RTL, producing unbounded proofs that run in about two hours and take less than a week to adapt to a new core. Applied to Rocket, Ri5CY and Pulpino, the flow finds real bugs — undocumented/added opcode behavior, FPU incorrect results, APB/AMBA protocol violations — and verifies 32/64‑bit implementations.

AI-written summary · about

" chapters (9)

1. 0:00Intro
2. 0:53Leading-Edge Technology Targeting critical hardware verification challenges
3. 2:06RISC-V Verification Challenges Does the RTL precisely implement the RISC-V ISA spec?
4. 2:55RISC-V Formal Methodology The specification
5. 5:45RISC-V Formal Methodology Pipelined processor verification
6. 6:24RISC-V Formal Methodology Interval Property Checking (IPC)
7. 8:20RISC-V Formal Methodology Automates and accelerates verification
8. 9:53Selection of Issues Found Rocket Core
9. 14:50More than a Core: Verifying RISC-V SoCs Summary

" related talks

• 13mIntroduction to RISC-V Processor VerificationLarry Lapides · embedded world 2022
• 25mRISC-V System-level Certification from Verification FoundationsAdnan Hamid · RISC-V Summit North America 2025
• 23mThe Continuum of RISC-V Compliance and Verification TestingSimon Davidmann, Allen Baum · RISC-V Summit 2022
• 12mRISC-V: Hardcore/Softcore Co-Simulation Environment with Cycle-Accurate RollbackJérémy Alcim · ORConf 2025
• 15mThe RISC-V Verification Ecosystem with Open Standards and Commercial ToolsJon Taylor · RISC-V Summit Europe 2023
• 47mTutorial: Choosing Appropriate Verification Techniques for Desired RISC...Aimee Sutton, Lee Moore · RISC-V Summit 2022
• 24mVerifying All the Flexibility of RISC-V within SoC DV Test PlansSimon Davidmann, Lee Moore · RISC-V Global Forum 2020
• 16mVerifying Out-Of-Order RISC-V Vector Extension With Open Source ToolsA. Kumar, S. Panandikar · RISC-V Summit North America 2025