[發(fā)明專(zhuān)利]一種驗(yàn)證Cache一致性協(xié)議的裝置及方法

有效

• 申請(qǐng)?zhí)枺?/td>: 201710601304.7
• 申請(qǐng)日: 2017-07-21
• 公開(kāi)（公告）號(hào): CN107368434B
• 公開(kāi)（公告）日: 2020-08-04
• 發(fā)明（設(shè)計(jì)）人: 王振江;周恒釗
• 申請(qǐng)（專(zhuān)利權(quán)）人: 蘇州浪潮智能科技有限公司
• 主分類(lèi)號(hào): G06F12/0815
• 分類(lèi)號(hào): G06F12/0815
• 代理公司: 濟(jì)南誠(chéng)智商標(biāo)專(zhuān)利事務(wù)所有限公司 37105
• 代理人: 王汝銀

1.一種驗(yàn)證Cache一致性協(xié)議的裝置，其特征是，所述的裝置包括：

形式驗(yàn)證平臺(tái)，利用驗(yàn)證平臺(tái)內(nèi)的驗(yàn)證工具，使用工具的內(nèi)部變量失效命令對(duì)模型初始表中的狀態(tài)變量進(jìn)行失效；

模型初始表，用來(lái)枚舉模型中的狀態(tài)變量并進(jìn)行初始狀態(tài)賦值；

模型其他表，包含協(xié)議說(shuō)明書(shū)或者說(shuō)明表的所有協(xié)議表，用來(lái)定義模型協(xié)議表之間跳轉(zhuǎn)接口，并實(shí)現(xiàn)模型協(xié)議表之間的跳轉(zhuǎn)驗(yàn)證；

模型規(guī)則定義表，用來(lái)定義模型協(xié)議表的跳轉(zhuǎn)規(guī)則，以及檢查Cache協(xié)議模型一致性；所述模型協(xié)議表的跳轉(zhuǎn)規(guī)則包括若干組變量狀態(tài)組合。

2.根據(jù)權(quán)利要求1所述的一種驗(yàn)證Cache一致性協(xié)議的裝置，其特征是，所述的模型初始表為模型協(xié)議表中的狀態(tài)表1。

3.根據(jù)權(quán)利要求1或2所述的一種驗(yàn)證Cache一致性協(xié)議的裝置，其特征是，所述模型初始表的初始狀態(tài)賦值為0。

4.一種驗(yàn)證Cache一致性協(xié)議的方法，其特征是，所述的方法包括以下步驟：

S1：執(zhí)行遍歷驗(yàn)證模式；

S2：判斷是否需要進(jìn)行隨機(jī)化驗(yàn)證，若是，進(jìn)入步驟S3，若否，返回步驟S1繼續(xù)執(zhí)行；

S3：利用驗(yàn)證失效命令，對(duì)模型初始表中的初始化變量進(jìn)行失效；

S4：?jiǎn)?dòng)模型規(guī)則定義表并隨機(jī)選取一組變量狀態(tài)組合；

S5：按照步驟S4中選取的變量狀態(tài)組合執(zhí)行跳轉(zhuǎn)驗(yàn)證。

5.根據(jù)權(quán)利要求4所述的一種驗(yàn)證Cache一致性協(xié)議的方法，其特征是，所述的方法還包括：

S6：對(duì)驗(yàn)證完成后模型協(xié)議表進(jìn)行統(tǒng)計(jì)，并計(jì)算模型驗(yàn)證的覆蓋率；

S7：重復(fù)步驟S4-S6，直至模型驗(yàn)證的覆蓋率為100％。

6.根據(jù)權(quán)利要求4或5所述的一種驗(yàn)證Cache一致性協(xié)議的方法，其特征是，步驟S1中，執(zhí)行遍歷驗(yàn)證模式的具體過(guò)程為：由模型初始表進(jìn)行觸發(fā)，模型中變量跳轉(zhuǎn)由零開(kāi)始，按照模型初始表中的變量狀態(tài)組合，模型其他表以傳統(tǒng)狀態(tài)機(jī)遍歷模式，從狀態(tài)1開(kāi)始對(duì)每個(gè)狀態(tài)進(jìn)行檢查驗(yàn)證。

7.根據(jù)權(quán)利要求4或5所述的一種驗(yàn)證Cache一致性協(xié)議的方法，其特征是，步驟S2的具體實(shí)現(xiàn)過(guò)程為：

設(shè)置一個(gè)標(biāo)準(zhǔn)驗(yàn)證時(shí)間，當(dāng)執(zhí)行遍歷驗(yàn)證模式的過(guò)程中，實(shí)時(shí)檢測(cè)某狀態(tài)的實(shí)際驗(yàn)證時(shí)間，當(dāng)檢測(cè)到實(shí)際驗(yàn)證時(shí)間超過(guò)標(biāo)準(zhǔn)驗(yàn)證時(shí)間，進(jìn)入步驟S3；

當(dāng)執(zhí)行遍歷驗(yàn)證模式結(jié)束后，計(jì)算模型驗(yàn)證的覆蓋率是否達(dá)到100％，若覆蓋率不足100％，進(jìn)入步驟S3，若覆蓋率達(dá)到100％，結(jié)束驗(yàn)證。