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