Breaking the RISC-V Processor Customization Barrier with Formal Verification

on YouTube ↗09m

" summary

Automated flow called Questa Processor takes ISA specs and generates an LTE formal model that verifies open-source cores like Rocket and CVA6, finds privilege-CSR and exception bugs and even a self-modifying code bug where stale decode data survives a refetch. Tool extracts CSRs, auto-generates assertions and witnesses, accepts custom instructions as SVA-like expressions, and yields exhaustive formal verification results; initial bug finds appear in about 3 days to initial findings, sign-off in weeks.

AI-written summary · about

" related talks

• 24mStrong Formal Verification For RISC V: From Instruction Set Manual To RTLAdam Chlipala · 7th RISC-V Workshop 2017
• 18mRISC-V Spotlight: Improving RISC-V Quality with Verification Standards and Advanc...Simon Davidmann · RISC-V Summit 2022
• 21mThe New Verification Ecosystem that Supports RISC-V Verification fo...Lee Moore, John Sotiropoulos · RISC-V Summit 2022
• 17mDemo: RISC-V Models for Verification, Software Development and Architectural Explor...Larry Lapides · RISC-V Summit 2022
• 11mDemo: More Than Point Tools: RISC-V SolutionsLarry Lapides · RISC-V Summit North America 2024
• 14mKeynote: Solving the Conundrum of Custom InstructionsSimon Davidmann · RISC-V Summit North America 2023
• 16mAutomatic Test Generation and Verification for RISC-V Vector ExtensionXi Wang, Shenwei Hu · RISC-V Summit 2022
• 01h 10mWhy RISC-V Through ISA Customization DemonstrationKeith Graham · RISC-V Summit North America 2023