Formal Verification of an Out-of-Order Multiprocessor against an In-Order Weak-Memory ISA

Janggun Lee, Jeehoon Kang

Out-of-order multiprocessor is a critical piece of modern hardware, and their verification must solve the following challenges. First, inter-core interleaving, in which the order t…