QED: Scalable Verification of Hardware Memory Consistency

Abstract

QED is a novel, scalable verification methodology designed to detect complex Memory Consistency Model (MCM) bugs in out-of-order (OOO) processors, surpassing the severe scaling limits of prior bounded verification techniques. It achieves scalability by focusing verification efforts only on directly-ordered instruction pairs and external coherence events, leveraging the principle that reordering is only a violation if a forbidden value is produced. The system automatically generates decision trees of simple predicates that check the RTL implementation, demonstrated successfully on complex models like RISC-V WMO using the BOOMv3 processor implementation.

Report

Key Highlights

• Scalable Verification: QED addresses the fundamental difficulty of verifying MCM compliance in high-performance out-of-order microprocessors, achieving scalability that moves beyond the practical limit of ~7 instructions faced by previous bounded verification methods.
• Focus on Observability: The core innovation is the notion of observability, arguing that hardware reordering only matters if it produces a forbidden execution value, simplifying the verification task.
• Optimized Search Space: Scalability is achieved by restricting analysis to only (1) directly-ordered instruction pairs (transitively non-redundant) and (2) the ordering of external events (e.g., invalidations) without tracking their originating cores.
• Automated Predicate Generation: The system automatically generates decision trees composed of simple, narrowly-defined predicates that must be evaluated against the Register Transfer Level (RTL) design.
• Practical Application: QED was successfully applied to generate verification criteria for established consistency models (SC, TSO) and the modern RISC-V Weak Memory Ordering (WMO) model, illustrating verification against the BOOMv3 RISC-V implementation.

Technical Details

• Target Component: Verification focuses specifically on the memory ordering logic within the out-of-order processor's Load-Store Queue (LSQ) and the coherence interface linking the core to global coherence mechanisms.
• MCM Models Supported: QED successfully generated verification decision trees for Sequential Consistency (SC), Total Store Ordering (TSO), and RISC-V Weak Memory Ordering (WMO).
• Verification Method: The method involves exhaustively exploring instruction pairs and intervening external events. For each permutation, QED attempts a transformation: restoring the reordered instructions back to an MCM-compliant order without altering the execution values. Failure to restore indicates an MCM violation.
• Predicate Structure: The output of QED's exploration is a decision tree where leaf nodes are simple Boolean predicates. These predicates must be evaluated against the RTL (e.g., checking specific queue state, fence status, or pending invalidations) to determine compliance.
• Experimental Target: The practical illustration of automatable verification involved evaluating a substantial predicate set against the open-source BOOMv3 implementation of the RISC-V architecture.

Implications

• Enabling Robust RISC-V OOO Designs: High-performance RISC-V cores rely on aggressive out-of-order execution and weak memory models (like WMO) for speed. QED provides a crucial, missing link for verifying these complex designs, ensuring that performance gains do not introduce insidious hardware bugs.
• Standardizing WMO Verification: As the RISC-V ecosystem matures, the RISC-V WMO model requires rigorous formal verification. QED provides the scalable tools necessary to formally guarantee compliance, increasing industry confidence in high-performance RISC-V implementations.
• Formal Verification Advancement: QED significantly pushes the boundary of formal verification in hardware architecture. By cleverly restricting the state space based on observability and relevant ordering dependencies, it makes verification of large, multi-core, out-of-order systems computationally tractable.
• Path to Automation: While the reported work illustrates predicate evaluation, QED's generation of structured decision trees paves the way for fully automated, integrated formal verification tools that can continuously check RTL changes for MCM violations during the development lifecycle.