Combined Dynamic and Formal Verification Approach to Processor Verification
summary
Combines Synopsys tools and workflows to find more bugs faster: unit-level formal using VC Formal and assertion IP (AIP) exhaustively checks buffers, decoder edge cases and arithmetic with DPV models; ISA-level uses lock-step continuous compare against a reference model to drive 100% functional coverage and reuse ELF tests across simulation, emulation and FPGA prototyping; multicore memory and coherence use on‑platform generation plus the FPV app to expose corner cases; examples on open-source cores CV32E40, CVW and CVA6 include bugs found in minutes.
AI-written summary · about
chapters (10)
- 0:00Introduction to verification approach
- 1:51Challenges in RISC-V verification
- 3:14Unit-level verification with formal
- 6:26Data path verification techniques
- 7:30ISA verification with dynamic methods
- 10:41ISA compliance with formal verification
- 13:34Verifying custom instructions and CSRs
- 16:02Processing subsystem verification
- 18:49Summary and benefits of combined approach
- 19:51Q&A session
related talks
13mIntroduction to RISC-V Processor Verification
17mDesign for Hardware Memory Model Verification
46mIntroduction to Formal Verification with Symbiotic EDA Open Source Tools
24mRISC V Processor Verification based on Open source Framework
47mTutorial: Choosing Appropriate Verification Techniques for Desired RISC...
23mCORE-V Verification Test Bench – Commercial Qualit...
19mThe role of software in validating silicon IP
23mThe Continuum of RISC-V Compliance and Verification Testing