【正文】 方法，實現(xiàn)了高效的面向并行計算機系統(tǒng)Cache 協(xié)議模型檢驗平臺，并能較好地擴展到大規(guī)模系統(tǒng)。 針對顯式模型檢驗工具可達(dá)狀態(tài)空間組織和維護(hù)存在的問題，本文提出了基于整型指針與Fibonacci 散列的可達(dá)狀態(tài)空間組織方法，實現(xiàn)了一 個高效的顯式模型檢驗原型系統(tǒng)，在確保驗證正確的同時有效縮短了驗證時間，并且在系統(tǒng)規(guī)范不可滿足的情況下能夠給出反例，有助于系統(tǒng)設(shè)計人員快速定位錯誤。 針對 Cache 協(xié)議狀態(tài)空間爆炸的問題，本文分析了并行應(yīng)用的數(shù)據(jù)訪問特性和共享模式，提出了共享集合偽臨界值的概念，有效優(yōu)化了目錄 Cache 協(xié)議狀態(tài)空間，并提出了解決小概率的寬共享事件的方法。實驗數(shù)據(jù)表明，基于偽臨界值的協(xié)議模型優(yōu)化，能夠有效縮小目錄 Cache 協(xié)議的狀態(tài)空間，加快驗證速度，提高驗證大規(guī)模 Cache協(xié)議的能力。 為支持可擴展 Cache 一致性協(xié)議 的驗證，本文提出了一個通用的參數(shù)化協(xié)議二維抽象框架 TDA，從構(gòu)成系統(tǒng)狀態(tài)空間的二維方向分別進(jìn)行抽象，最大限度地剔除了原始系統(tǒng)中的冗余信息。 TDA 模型關(guān)于單索引 ACTL*公式弱保持，足以驗證原始系統(tǒng)。建立的具有真并發(fā)語義的參數(shù)化系統(tǒng)的形式化模型，適合描述一般意義上的并發(fā)系統(tǒng)，更具通用性和適用性。理論推導(dǎo)和 Cache 一致性協(xié)議抽象實例都驗證了 TDA 的正確性和合理性。 針對面向協(xié)議實現(xiàn)級的低層次驗證脫節(jié)問題，本文開展了 RTL 級 Cache 一致性協(xié)議模型檢驗研究。在決策圖模型的基礎(chǔ)上，提出了利用約束邏輯編程對協(xié)議 的 Verilog 描述進(jìn)行謂詞抽象的方法。與基于 SAT 的方法相比，不需要將字級約束展開為位級約束，求解效率顯著提高，并且提供了一個統(tǒng)一的框架用于描述各種約束。 結(jié)合工程需要，本文研究了高性能計算機的 Cache 一致性協(xié)議模型，以及協(xié)議的主要特點與主要性質(zhì)，構(gòu)建了面向高性能計算機的 Cache 協(xié)議模型檢驗平臺 HVPCP，從高層協(xié)議級與 RTL 實現(xiàn)級兩個層次實現(xiàn) Cache 一致性協(xié)議的顯式和隱式模型檢驗。 Cache 一致性協(xié)議是實現(xiàn)多處理機系統(tǒng)的關(guān)鍵，不僅直接決定多處理機系統(tǒng)的正確性，而且對系統(tǒng)的規(guī)模和性能有著至關(guān)重 要的影響。日益增大的系統(tǒng)規(guī)模、存儲一致性模型的多樣性、互連網(wǎng)絡(luò)延遲的不確定性、多核技術(shù)的迅猛發(fā)展等諸多因素交織在一起，使 Cache 一致性協(xié)議異常復(fù)雜，協(xié)議的狀態(tài)空間出現(xiàn)爆炸，導(dǎo)致 Cache 一致性協(xié)議的功能驗證非常困難，面臨許多迫切需要解決的技術(shù)問題。 論文針對 Cache 一致性協(xié)議驗證中的狀態(tài)空間爆炸問題，結(jié)合新一代高效能并行計算機系統(tǒng)的研制，開展 Cache 一致性協(xié)議模型檢驗關(guān)鍵技術(shù)的研究。以建立基于二維抽象的模型檢驗理論框架體系為目標(biāo)，面向顯式和隱式兩種模式、高層協(xié)議級和低層實現(xiàn)級兩個層次，多角度展開研 究，利用并行應(yīng)用的數(shù)據(jù)訪問特性和共享模式等領(lǐng)域知識設(shè)計恰當(dāng)?shù)膬?yōu)化方法，實現(xiàn)了高效的面向并行計算機系統(tǒng)Cache 協(xié)議模型檢驗平臺，并能較好地擴展到大規(guī)模系統(tǒng)。 針對顯式模型檢驗工具可達(dá)狀態(tài)空間組織和維護(hù)存在的問題，本文提出了基于整型指針與Fibonacci 散列的可達(dá)狀態(tài)空間組織方法，實現(xiàn)了一個高效的顯式模型檢驗原型系統(tǒng)，在確保驗證正確的同時有效縮短了驗證時間，并且在系統(tǒng)規(guī)范不可滿足的情況下能夠給出反例，有助于系統(tǒng)設(shè)計人員快速定位錯誤。 針對 Cache 協(xié)議狀態(tài)空間爆炸的問題，本文分析了并行應(yīng)用的數(shù)據(jù)訪問 特性和共享模式，提出了共享集合偽臨界值的概念，有效優(yōu)化了目錄 Cache 協(xié)議狀態(tài)空間，并提出了解決小概率的寬共享事件的方法。實驗數(shù)據(jù)表明，基于偽臨界值的協(xié)議模型優(yōu)化，能夠有效縮小目錄 Cache 協(xié)議的狀態(tài)空間，加快驗證速度，提高驗證大規(guī)模 Cache協(xié)議的能力。 為支持可擴展 Cache 一致性協(xié)議的驗證，本文提出了一個通用的參數(shù)化協(xié)議二維抽象框架 TDA，從構(gòu)成系統(tǒng)狀態(tài)空間的二維方向分別進(jìn)行抽象，最大限度地剔除了原始系統(tǒng)中的冗余信息。 TDA 模型關(guān)于單索引 ACTL*公式弱保持，足以驗證原始系統(tǒng)。建立的具有真并發(fā)語義 的參數(shù)化系統(tǒng)的形式化模型，適合描述一般意義上的并發(fā)系統(tǒng)，更具通用性和適用性。理論推導(dǎo)和 Cache 一致性協(xié)議抽象實例都驗證了 TDA 的正確性和合理性。 針對面向協(xié)議實現(xiàn)級的低層次驗證脫節(jié)問題，本文開展了 RTL 級 Cache 一致性協(xié)議模型檢驗研究。在決策圖模型的基礎(chǔ)上，提出了利用約束邏輯編程對協(xié)議的 Verilog 描述進(jìn)行謂詞抽象的方法。與基于 SAT 的方法相比，不需要將字級約束展開為位級約束，求解效率顯著提高，并且提供了一個統(tǒng)一的框架用于描述各種約束。 結(jié)合工程需要，本文研究了高性能計算機的 Cache 一致性協(xié) 議模型，以及協(xié)議的主要特點與主要性質(zhì)，構(gòu)建了面向高性能計算機的 Cache 協(xié)議模型檢驗平臺 HVPCP，從高層協(xié)議級與 RTL 實現(xiàn)級兩個層次實現(xiàn) Cache 一致性協(xié)議的顯式和隱式模型檢驗。 Cache 一致性協(xié)議是實現(xiàn)多處理機系統(tǒng)的關(guān)鍵，不僅直接決定多處理機系統(tǒng)的正確性，而且對系統(tǒng)的規(guī)模和性能有著至關(guān)重要的影響。日益增大的系統(tǒng)規(guī)模、存儲一致性模型的多樣性、互連網(wǎng)絡(luò)延遲的不確定性、多核技術(shù)的迅猛發(fā)展等諸多因素交織在一起，使 Cache 一致性協(xié)議異常復(fù)雜，協(xié)議的狀態(tài)空間出現(xiàn)爆炸，導(dǎo)致 Cache 一致性協(xié)議的功能驗證非常困難， 面臨許多迫切需要解決的技術(shù)問題。 論文針對 Cache 一致性協(xié)議驗證中的狀態(tài)空間爆炸問題，結(jié)合新一代高效能并行計算機系統(tǒng)的研制，開展 Cache 一致性協(xié)議模型檢驗關(guān)鍵技術(shù)的研究。以建立基于二維抽象的模型檢驗理論框架體系為目標(biāo)，面向顯式和隱式兩種模式、高層協(xié)議級和低層實現(xiàn)級兩個層次，多角度展開研究，利用并行應(yīng)用的數(shù)據(jù)訪問特性和共享模式等領(lǐng)域知識設(shè)計恰當(dāng)?shù)膬?yōu)化方法，實現(xiàn)了高效的面向并行計算機系統(tǒng)Cache 協(xié)議模型檢驗平臺，并能較好地擴展到大規(guī)模系統(tǒng)。 針對顯式模型檢驗工具可達(dá)狀態(tài)空間組織和維護(hù)存在的問題，本 文提出了基于整型指針與Fibonacci 散列的可達(dá)狀態(tài)空間組織方法，實現(xiàn)了一個高效的顯式模型檢驗原型系統(tǒng)，在確保驗證正確的同時有效縮短了驗證時間，并且在系統(tǒng)規(guī)范不可滿足的情況下能夠給出反例，有助于系統(tǒng)設(shè)計人員快速定位錯誤。 針對 Cache 協(xié)議狀態(tài)空間爆炸的問題，本文分析了并行應(yīng)用的數(shù)據(jù)訪問特性和共享模式，提出了共享集合偽臨界值的概念，有效優(yōu)化了目錄 Cache 協(xié)議狀態(tài)空間，并提出了解決小概率的寬共享事件的方法。實驗數(shù)據(jù)表明，基于偽臨界值的協(xié)議模型優(yōu)化，能夠有效縮小目錄 Cache 協(xié)議的狀態(tài)空間，加快驗證速度 ，提高驗證大規(guī)模 Cache協(xié)議的能力。 為支持可擴展 Cache 一致性協(xié)議的驗證，本文提出了一個通用的參數(shù)化協(xié)議二維抽象框架 TDA，從構(gòu)成系統(tǒng)狀態(tài)空間的二維方向分別進(jìn)行抽象，最大限度地剔除了原始系統(tǒng)中的冗余信息。 TDA 模型關(guān)于單索引 ACT