Fast Verification of Memory Consistency for Chip Multi-Processor

Verifying the execution of a test program against the memory consistency model is known to be NP-hard. Because of lacking extra observability, verifying the memory consistency model in post-silicon stage is even harder than in pre-silicon stage. In this paper, by identifying the pending windows of microprocessor and introducing the resultant time order restrictions, we propose a low time complexity algorithm for checking end-to-end correctness on real systems. Our MOTEC tool, which implements the above algorithm, has been successfully detected several injected bugs in a CMP emulation environment. It is also worth noting that MOTEC is general enough to support many CMP systems with trivial modifications.