Model checking MESIF Cache coherence protocol
Yi Lv · Computer Engineering and Applications Journal · 2010
The scaling limitations of uniprocessors have led to an industry-wide turn towards Chip MultiProcessor(CMP) systems.To obtain better performance and scalability,cache coherence protocol of CMP systems is becoming increasingly complex.The verification of cache coherence protocol is one of the classic applications of model checking,and more efficient model checking methods are developed for it.Cache coherence protocol model checking at the micro architecture level models message queues and control structures and is more complex than architecture level.A cache coherence protocol of Intel is modeled at micro architecture level.Therefore this protocol is model checked by NuSMV tool.