【摘要】：隨著集成電路工藝水平的不斷提升，多核處理器已成為高性能微處理器的主流結(jié)構(gòu)。為緩解處理器核心與存儲(chǔ)器之間不斷擴(kuò)大的速度差異，引入Cache來解決這一問題。然而，Cache在提高性能的同時(shí)，也帶來數(shù)據(jù)的不一致性問題。目前普遍采用Cache一致性協(xié)議來保證多核處理器間共享數(shù)據(jù)的一致性。Cache一致性協(xié)議設(shè)計(jì)和實(shí)現(xiàn)的正確性不僅決定了多核處理器功能的正確性，而且對(duì)整個(gè)處理器規(guī)模和性能都有著至關(guān)重要的影響。因此，必須對(duì)Cache一致性協(xié)議的功能正確性進(jìn)行全面而有效地驗(yàn)證。 本文以SystemC語言描述的多核處理器Cache一致性協(xié)議為研究對(duì)象，采用形式化驗(yàn)證方法中運(yùn)用最為普遍的模型檢驗(yàn)技術(shù)完成協(xié)議驗(yàn)證工作。設(shè)計(jì)并實(shí)現(xiàn)一個(gè)針對(duì)硬件描述語言的模型檢驗(yàn)平臺(tái)，能夠很好的應(yīng)用于多核處理器Cache一致性協(xié)議驗(yàn)證。 針對(duì)多核處理器Cache一致性協(xié)議構(gòu)成的參數(shù)化系統(tǒng)的驗(yàn)證問題，提出基于謂詞的自動(dòng)化抽象方法，從待驗(yàn)證的性質(zhì)出發(fā)對(duì)參數(shù)化系統(tǒng)進(jìn)行抽象建模與化簡(jiǎn)，有效壓縮了狀態(tài)空間。研究成果應(yīng)用到經(jīng)典的Cache一致性協(xié)議和FT-1000CPU協(xié)議的驗(yàn)證，取得了很好的效果。 針對(duì)符號(hào)遷移系統(tǒng)到Kripke結(jié)構(gòu)的模型轉(zhuǎn)換問題，提出新的模型轉(zhuǎn)換算法，，能夠生成更小規(guī)模的Kripke結(jié)構(gòu)。完成了算法的設(shè)計(jì)和實(shí)現(xiàn)，實(shí)驗(yàn)結(jié)果表明新的算法比原始算法在性能上有很大提升。
[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.
【學(xué)位授予單位】：國(guó)防科學(xué)技術(shù)大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2012
【分類號(hào)】：TP332

【參考文獻(xiàn)】

相關(guān)期刊論文 前2條

1 屈婉霞;龐征斌;郭陽;李暾;楊曉東;;參數(shù)化系統(tǒng)二維抽象框架[J];國(guó)防科技大學(xué)學(xué)報(bào);2010年01期

2 楊學(xué)軍;廖湘科;盧凱;胡慶豐;宋君強(qiáng);蘇金樹;;The TianHe-1A Supercomputer: Its Hardware and Software[J];Journal of Computer Science & Technology;2011年03期

本文編號(hào)：2381735