QED: Scalable Verification of Hardware Memory Consistency

TL;DR

This work addresses the challenge of verifying memory consistency in out-of-order, multi-core systems, where exhaustive verification scales poorly with in-flight instructions and core count. It introduces QED, an observability-based approach that focuses on directly-ordered instruction pairs connected by edges in the memory-consistency model (MCM) and on external events from other cores, enabling scalable exploration with complexity $O(m^2 e^2)$. The method decomposes verification into exhaustive pairwise-order explorations with restoration to MCM-compliant orders, followed by predicate evaluation against RTL; the authors automate tree generation for SC, TSO, and RVWMO and demonstrate a substantial predicate test on BOOM v3. The significance lies in delivering a scalable path toward automatic hardware verification of memory ordering in modern out-of-order processors, potentially enabling more reliable design without hardware overhead, with full automation of predicate evaluation identified as future work.

Abstract

Memory consistency model (MCM) issues in out-of-order-issue microprocessor-based shared-memory systems are notoriously non-intuitive and a source of hardware design bugs. Prior hardware verification work is limited to in-order-issue processors, to proving the correctness only of some test cases, or to bounded verification that does not scale in practice beyond 7 instructions across all threads. Because cache coherence (i.e., write serialization and atomicity) and pipeline front-end verification and testing are well-studied, we focus on the memory ordering in an out-of-order-issue processor's load-store queue and the coherence interface between the core and global coherence. We propose QED based on the key notion of observability that any hardware reordering matters only if a forbidden value is produced. We argue that one needs to consider (1) only directly-ordered instruction pairs -- transitively non-redundant pairs connected by an edge in the MCM-imposed partial order -- and not all in-flight instructions, and (2) only the ordering of external events from other cores (e.g.,invalidations) but not the events' originating cores, achieving verification scalability in both the numbers of in-flight memory instructions and of cores. Exhaustively considering all pairs of instruction types and all types of external events intervening between each pair, QED attempts to restore any reordered instructions to an MCM-complaint order without changing the execution values, where failure indicates an MCM violation. Each instruction pair's exploration results in a decision tree of simple, narrowly-defined predicates to be evaluated against the RTL. In our experiments, we automatically generate the decision trees for SC, TSO, and RISC-V WMO, and illustrate automatable verification by evaluating a substantial predicate against BOOMv3 implementation of RISC-V WMO, leaving full automation to future work.

Figures (8)

• Figure 1: SC example restoration
• Figure 2: Data path of loads (red,blue) and stores (green,blue).
• Figure 3: QED
• Figure 4: Example restoration
• Figure 5: Exploration tree for ld-ld ordering in SC showing only invalidations