A simulation-based approach to architectural verification of multiprocessor systems

This paper presents a simulation-based method for verifying coherency in weakly ordered shared memory multiprocessor systems. This methodology requires minimal assumptions regarding the implementation details, such as the coherence protocol and cache line replacement rules. Independence from implementation details for architectural verification is achieved via a technique called data-coloring. The non-determinism arising from weak ordering is resolved by introducing the notion of valid sets for checking the correctness of memory operations. We contrast our approach with other methods that have been prevalent in the industry and provide implementation details and an example implementation of our methodology