QED: Scalable Consistency Verification of Memory Instruction Reordering in Hardware

Memory consistency models (MCMs) in out-oforder-issue microprocessor-based shared-memory systems are notoriously non-intuitive and a source of hardware design bugs. Previous hardware verification work is limited to (1) in-orderissue processors, (2) proving the correctness only for some test cases, or (3) bounded verification that does not scale in practice beyond 7 instructions across all threads. Because cache coherence (i.e., write serialization and (non-)multi-copy write atomicity) and pipeline front-end verification and testing are well-studied, we focus on memory instruction ordering in the load-store queue (LSQ) of an out-of-order-issue processor. We show that our approach, called QED, needs to consider (1) only a small subset of instruction pairs and not all in-flight instructions, and (2) only one external event from other cores at a time per instruction of a pair (e.g., an invalidation), where only the events' ordering matters but not their originating cores. We call these results as two+two. Exhaustively exploring all pairs of instruction types and all types of event pairs intervening between each instruction pair, QED checks whether each of a reordered pair's execution trace leads to a cycle, which is well known to indicate an MCM violation. The MCM-violating execution traces in each instruction pair's exploration result in a decision tree of simple, narrowlydefined predicates to be evaluated in the RTL implementation. Our two+two result proves that the number of predicates for all MCMs is independent of program length and of the numbers of in-flight memory instructions and cores. Nevertheless, each predicate must explore all of the LSQ's RTL state. To combat RTL state space explosion, QED employs novel, empirical state space reduction, which itself is verified, to remain scalable for practical design sizes. In our experiments, we automatically generate the decision trees for SC, TSO, and RISC-V WMO, and verify the LSQ of BOOMv3 RTL with 128 loads/64 stores against RISC-V WMO using Jaspergold, where we found two correctness bugs and a performance bug (though not our goal). We fully verify the corrected implementation in under ten days. This unbounded RTL verification of a modern out-of-order-issue processor's LSQ against an MCM is the first in the literature.