# QED: Scalable Verification of Hardware Memory Consistency

**Authors:** Gokulan Ravi, Xiaokang Qiu, Mithuna Thottethodi, T. N. Vijaykumar  
**arXiv:** [2404.03113](https://arxiv.org/abs/2404.03113)  
**Date:** 2024-04-03  
**Summary page:** https://www.summarizepaper.com/en/paper/2404.03113v1/

## Key points

- Authors address complex issues surrounding memory consistency models (MCM) in out-of-order-issue microprocessor-based shared-memory systems
- Previous hardware verification efforts focused on in-order-issue processors or specific test cases, lacking scalability
- QED introduced as a solution based on observability to detect forbidden values resulting from hardware reordering
- Scalability achieved by considering directly-ordered instruction pairs and focusing on the ordering of external events from other cores
- Verification process involves exploring reorderings through decision trees with simple predicates evaluated against RTL
- Automated generation of decision trees for SC, TSO, and RISC-V WMO models demonstrated
- Research offers insights into scalable hardware memory consistency verification methods for out-of-order-issue processors

## Summary

In their paper titled "QED: Scalable Verification of Hardware Memory Consistency," authors Gokulan Ravi, Xiaokang Qiu, Mithuna Thottethodi, and T. N. Vijaykumar address the complex issues surrounding memory consistency models (MCM) in out-of-order-issue microprocessor-based shared-memory systems. These issues are known to be non-intuitive and often lead to hardware design bugs. Previous hardware verification efforts have primarily focused on in-order-issue processors or limited themselves to proving the correctness of specific test cases, resulting in bounded verification that lacks scalability beyond a certain number of instructions across all threads. The authors concentrate on the memory ordering within an out-of-order-issue processor's load-store queue and the coherence interface between the core and global coherence. This is because cache coherence and pipeline front-end verification have been extensively studied. They introduce QED as a solution based on the concept of observability, asserting that any hardware reordering is significant only if it results in a forbidden value being produced. To achieve scalability in verification, the authors propose considering only directly-ordered instruction pairs – those connected by an edge in the MCM-imposed partial order – rather than analyzing all in-flight instructions. They also suggest focusing solely on the ordering of external events from other cores (e.g., invalidations) rather than considering the events' originating cores. By exhaustively examining all pairs of instruction types and external events between each pair, QED aims to restore any reordered instructions to an MCM-compliant order without altering execution values. The verification process involves exploring each instruction pair's possible reorderings through decision trees consisting of simple predicates evaluated against Register Transfer Language (RTL). The authors demonstrate automated generation of decision trees for Sequential Consistency (SC), Total Store Order (TSO), and RISC-V Weak Memory Ordering (WMO) models. They showcase automatable verification by evaluating a substantial predicate against the BOOMv3 implementation of RISC-V WMO, leaving room for further automation enhancements in future work. Overall, this research contributes valuable insights into scalable hardware memory consistency verification methods for out-of-order-issue processors, offering a systematic approach to identifying and rectifying potential MCM violations without compromising execution values.