多核处理器Cache一致性协议模型检验研究与实现
发布时间：2018-12-16 03:07
【摘要】：随着集成电路工艺水平的不断提升，多核处理器已成为高性能微处理器的主流结构。为缓解处理器核心与存储器之间不断扩大的速度差异，引入Cache来解决这一问题。然而，Cache在提高性能的同时，也带来数据的不一致性问题。目前普遍采用Cache一致性协议来保证多核处理器间共享数据的一致性。Cache一致性协议设计和实现的正确性不仅决定了多核处理器功能的正确性，而且对整个处理器规模和性能都有着至关重要的影响。因此，必须对Cache一致性协议的功能正确性进行全面而有效地验证。 本文以SystemC语言描述的多核处理器Cache一致性协议为研究对象，采用形式化验证方法中运用最为普遍的模型检验技术完成协议验证工作。设计并实现一个针对硬件描述语言的模型检验平台，能够很好的应用于多核处理器Cache一致性协议验证。 针对多核处理器Cache一致性协议构成的参数化系统的验证问题，提出基于谓词的自动化抽象方法，从待验证的性质出发对参数化系统进行抽象建模与化简，有效压缩了状态空间。研究成果应用到经典的Cache一致性协议和FT-1000CPU协议的验证，取得了很好的效果。 针对符号迁移系统到Kripke结构的模型转换问题，提出新的模型转换算法，，能够生成更小规模的Kripke结构。完成了算法的设计和实现，实验结果表明新的算法比原始算法在性能上有很大提升。
[Abstract]:With the continuous improvement of integrated circuit technology, multi-core processors have become the mainstream architecture of high-performance microprocessors. In order to alleviate the increasing speed difference between processor core and memory, Cache is introduced to solve this problem. However, Cache not only improves performance, but also brings inconsistency of data. At present, Cache conformance protocol is widely used to ensure the consistency of shared data among multi-core processors. The correctness of design and implementation of Cache conformance protocol not only determines the correctness of multi-core processor function. And it has a crucial impact on the size and performance of the entire processor. Therefore, the functional correctness of Cache conformance protocol must be verified comprehensively and effectively. In this paper, the multi-core processor Cache conformance protocol described in SystemC language is taken as the research object, and the most popular model checking technique is used in the formal verification method to complete the protocol verification. A model checking platform for hardware description language is designed and implemented, which can be applied to the verification of multi-core processor Cache conformance protocol. Aiming at the verification problem of parameterized system based on multi-core processor Cache conformance protocol, an automatic abstraction method based on predicate is proposed. The abstract modeling and simplification of parameterized system are carried out based on the properties to be verified, and the state space is effectively compressed. The research results are applied to the verification of classical Cache conformance protocol and FT-1000CPU protocol, and good results are obtained. To solve the problem of model transformation from symbol migration system to Kripke structure, a new model transformation algorithm is proposed, which can generate a smaller Kripke structure. The design and implementation of the algorithm are completed. The experimental results show that the performance of the new algorithm is much better than that of the original algorithm.
【学位授予单位】：国防科学技术大学
【学位级别】：硕士
【学位授予年份】：2012
【分类号】：TP332
本文编号：2381735
[Abstract]:With the continuous improvement of integrated circuit technology, multi-core processors have become the mainstream architecture of high-performance microprocessors. In order to alleviate the increasing speed difference between processor core and memory, Cache is introduced to solve this problem. However, Cache not only improves performance, but also brings inconsistency of data. At present, Cache conformance protocol is widely used to ensure the consistency of shared data among multi-core processors. The correctness of design and implementation of Cache conformance protocol not only determines the correctness of multi-core processor function. And it has a crucial impact on the size and performance of the entire processor. Therefore, the functional correctness of Cache conformance protocol must be verified comprehensively and effectively. In this paper, the multi-core processor Cache conformance protocol described in SystemC language is taken as the research object, and the most popular model checking technique is used in the formal verification method to complete the protocol verification. A model checking platform for hardware description language is designed and implemented, which can be applied to the verification of multi-core processor Cache conformance protocol. Aiming at the verification problem of parameterized system based on multi-core processor Cache conformance protocol, an automatic abstraction method based on predicate is proposed. The abstract modeling and simplification of parameterized system are carried out based on the properties to be verified, and the state space is effectively compressed. The research results are applied to the verification of classical Cache conformance protocol and FT-1000CPU protocol, and good results are obtained. To solve the problem of model transformation from symbol migration system to Kripke structure, a new model transformation algorithm is proposed, which can generate a smaller Kripke structure. The design and implementation of the algorithm are completed. The experimental results show that the performance of the new algorithm is much better than that of the original algorithm.
【学位授予单位】：国防科学技术大学
【学位级别】：硕士
【学位授予年份】：2012
【分类号】：TP332
【参考文献】
相关期刊论文 前2条
1 屈婉霞;庞征斌;郭阳;李暾;杨晓东;;参数化系统二维抽象框架[J];国防科技大学学报;2010年01期
2 杨学军;廖湘科;卢凯;胡庆丰;宋君强;苏金树;;The TianHe-1A Supercomputer: Its Hardware and Software[J];Journal of Computer Science & Technology;2011年03期
本文编号：2381735
本文链接：https://www.wllwen.com/kejilunwen/jisuanjikexuelunwen/2381735.html
