Directed Test Generation for Validation of Cache Coherence Protocols

作者：Lyu, Yangdi^*; Qin, Xiaoke; Chen, Mingsong; Mishra, Prabhat

来源：IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2019, 38(1): 163-176.

DOI：10.1109/TCAD.2018.2801239

• Cache coherence
• quotient space
• test generation
• verification

Computing systems utilize multicore processors with complex cache coherence protocols to meet the increasing need for performance and energy improvement. It is a major challenge to verify the correctness of a cache coherence protocol since the number of reachable states grows exponentially with the number of cores. In this paper, we propose an efficient test generation technique, which can be used to achieve full state and transition coverage in simulation-based verification for a wide variety of cache coherence protocols. Based on effective analysis of the state space structure, our method can generate more efficient test sequences (50% shorter) on-the-fly compared with tests generated by BFS. While our on-the-fly method can reduce the numbers of required tests by half, it can still be impractical to verify all possible transitions in the presence of large number of cores. We propose scalable on-the-fly test generation techniques using quotient state space. The proposed approach guarantees selection of important transitions by utilizing equivalence classes, and omits only similar transitions. Our experimental results demonstrate that our proposed approaches can efficiently tradeoff between transition coverage and validation effort.

• 出版日期2019-1
• 单位华东师范大学