Design for Hardware Memory Model Verification
summary
Toolchain synthesizes an axiomatic MCM from SystemVerilog netlist using static netlist analysis, property generation and model checking, producing a model rtl2$\mu$spec claims is correct by construction and plugs into existing formal MCM flows; a case study on a four-core RISC-V multi-V-scale design verifies sequential consistency. Current gaps are limited support for out-of-order execution, speculation, caches and coherence and many properties return undetermined; proposed DFV adds small runtime FSM monitors and uses CEGAR to minimize inserted hardware.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 0:20Concurrent program
- 0:43Memory Consistency Model
- 1:35Verification Approach
- 3:51Mixedback Model
- 9:30Scalability
- 16:11Conclusion
related talks
21mCombined Dynamic and Formal Verification Approach to Processor Verification
16mSoftware Development for 64-Bit RISC-V Processor Verification
25mRISC-V System-level Certification from Verification Foundations
09mLightning Talk: Design Verification with Step-and-Compare for RISC-V...
14mSVM: A Synthesizable Approach to Efficient RISC-V CPU Verification
24mRISC V Processor Verification based on Open source Framework
13mIntroduction to RISC-V Processor Verification
12mRISC-V: Hardcore/Softcore Co-Simulation Environment with Cycle-Accurate Rollback