Explore a 17-minute conference talk from ACM SIGPLAN on designing hardware memory model verification. Delve into the bottom-up approach called rtl2$\mu$spec, which synthesizes an axiomatic model of Memory Consistency Model (MCM) implementation directly from SystemVerilog design. Learn about the challenges in scaling this approach to support advanced processor designs with features like out-of-order execution, speculation, and caches. Discover the steps taken towards addressing model-checker limitations through design-for-verification techniques. Gain insights into the efficiency and scalability improvements demonstrated in a case study on a four-core RISC-V multi-V-scale processor implementing sequential consistency.
Overview
Syllabus
Introduction
Concurrent program
Memory Consistency Model
Verification Approach
Mixedback Model
Scalability
Conclusion
Taught by
ACM SIGPLAN
