BatchSolve: A Divide and Conquer Approach to Solving the Memory Ordering Problem
In this paper, we introduce Batch-Solve (BATS) – a low-cost, robust, scalable, portable, and flexible approach to solving the Memory Ordering Problem (MOP), which is a crucial to memory subsystem verification. By formulating the MOP as a batch-wise constraint randomization problem, we provide a methodology in which we can verify whether the memory ordering of racing true shared stimulus violate any of the memory ordering rules without the heavy overhead of transaction tracking. By leveraging the power of System Verilog (SV) constraint randomizer we allow users to specify ordering rules as high-level SV constraints, thereby avoiding checker implementation bugs. We provide an infrastructure which can be easily ported over to another TB (horizontal re-use) and is immune to architectural modifications (vertical re-use across projects). To the best of our knowledge, this is the first System Verilog Solver based approach to solving the MOP.