Title :
Hierarchical cache coherence protocol verification one level at a time through assume guarantee
Author :
Xiaofang Chen ; Yu Yang ; Delisi, Michael ; Gopalakrishnan, Ganesh ; Ching-Tsun Chou
Author_Institution :
Univ. of Utah, Salt Lake City
Abstract :
Due to the error-prone nature of modern cache coherence protocols, in all modern processor design flows these protocols are formally specified at the level of interleaving atomic transactions and model checked. Explicit state enumeration methods are almost always used for coherence protocol verification, as symbolic methods have failed to deliver advantages in this area. The move towards multicores implies that hierarchical organizations of several different cache coherence protocols will be employed in the future. The product state space of all these protocols jointly operating in a multicore cache hierarchy is beyond the reach of all available explicit state model checkers. In our previous work, an assume guarantee technique that allowed these protocols to be handled for the first time was reported. In this approach, a method was proposed to create a set of initial abstract protocols Mi % where each Mi simulates the given hierarchical protocol. After the set of initial Mi´s are created, verification consists of dealing with Mi´s in an assume guarantee manner, refining each Mi in the process. The drawbacks of this work were: (i) even a single Mt modeled more than one level of the coherence protocols, thus still creating very large product spaces; (ii) details such as non-inclusive caching hierarchies could not be handled; (iii) the initial Mi´s were created manually, which is tedious and error prone. This paper overcomes all these limitations, handling non-inclusive caching hierarchies, bringing about a 95% reduction in the total state space encountered during any single explicit enumeration search, and requiring only a few such runs to finish verification.
Keywords :
cache storage; formal verification; interleaved storage; memory protocols; microprocessor chips; multiprocessing systems; assume guarantee; atomic transaction interleaving; error-prone nature; explicit state enumeration method; explicit state model checker; hierarchical cache coherence protocol verification; modern processor design flow; multicore cache hierarchy; product state space; Binary decision diagrams; Cities and towns; Coherence; Concurrent computing; Interleaved codes; Manufacturing; Multicore processing; Process design; Protocols; State-space methods;
Conference_Titel :
High Level Design Validation and Test Workshop, 2007. HLVDT 2007. IEEE International
Conference_Location :
Irvine, CA
Print_ISBN :
978-1-4244-1480-2
DOI :
10.1109/HLDVT.2007.4392796