Design for Hardware Memory Model Verification - PLARCH23

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.

Introduction
Concurrent program
Memory Consistency Model
Verification Approach
Mixedback Model
Scalability
Conclusion