本發(fā)明提供了一種驗證Cache一致性協(xié)議的裝置,所述的裝置包括:形式驗證平臺,利用驗證平臺內(nèi)的驗證工具,使用工具的內(nèi)部變量失效命令對模型初始表中的狀態(tài)變量進行失效;模型初始表,用來枚舉模型中的狀態(tài)變量并進行初始狀態(tài)賦值;模型其他表,包含協(xié)議說明書或者說明表的所有協(xié)議表,用來定義模型協(xié)議表之間跳轉(zhuǎn)接口,并實現(xiàn)模型協(xié)議表之間的跳轉(zhuǎn)驗證;模型規(guī)則定義表,用來定義模型協(xié)議表的跳轉(zhuǎn)規(guī)則,以及檢查Cache協(xié)議模型一致性。通過對模型中的變量狀態(tài)進行組合,增加驗證工具的驗證路徑,縮短驗證時間?;谘b置,本發(fā)明還提供了一種驗證Cache一致性協(xié)議的方法。
聲明:
“驗證Cache一致性協(xié)議的裝置及方法” 該技術(shù)專利(論文)所有權(quán)利歸屬于技術(shù)(論文)所有人。僅供學習研究,如用于商業(yè)用途,請聯(lián)系該技術(shù)所有人。
我是此專利(論文)的發(fā)明人(作者)