[發明專利]設備規范與設備行為的一致性檢測系統

無效

• 申請號: 201110391203.4
• 申請日: 2011-11-30
• 公開（公告）號: CN102495766A
• 公開（公告）日: 2012-06-13
• 發明（設計）人: 胡事民;馬超;湯茂杰
• 申請（專利權）人: 清華大學
• 主分類號: G06F11/00
• 分類號: G06F11/00
• 代理公司: 北京路浩知識產權代理有限公司 11002
• 代理人: 王瑩

技術領域

本發明涉及設備規范及設備行為的可靠性技術領域，尤其涉及一種設備規范與設備行為的一致性檢測系統。

背景技術

可靠性是操作系統的一個重要目標。Windows?XP操作系統85％的失效是由設備驅動造成的。Linux操作系統設備驅動失效的頻率是其它部分的3-7倍以上。驅動編寫人員根據設備規范進行設備驅動的編寫，因此，設備規范和硬件設備行為的一致性對于設備驅動的可靠性具有重要意義。

發明內容

(一)要解決的技術問題

本發明要解決的技術問題是：提供一種設備規范與設備行為的一致性檢測系統，其能夠檢測設備規范與設備行為的一致性，從而可以提高設備規范和設備驅動的可靠性。

(二)技術方案

為解決上述問題，本發明提供了一種設備規范與設備行為的一致性檢測系統，包括：

設備規范轉化模塊，用于將Termite語言描述的設備規范轉化為模型檢測工具能夠識別的UCLID語言描述的設備規范；

設備行為轉化模塊，用于將Verilog語言描述的硬件設備行為轉化為UCLID語言描述的硬件設備行為；

一致性檢測模塊，用于將所述UCLID語言描述的設備規范和硬件設備行為輸入模型檢測工具得出檢測結果。

優選地，所述設備規范轉化模塊包括：

變量轉化模塊，用于將使用的Termite語言的變量轉化為UCLID語言的變量；

常數轉化模塊，用于將使用的Termite語言的常數轉化為UCLID語言的常數；

操作命令轉化模塊，用于將使用的Termite語言的操作命令轉化為UCLID語言的FUNC和PRED操作命令函數。

優選地，所述變量轉化模塊包括：

枚舉類型轉化模塊，用于將Termite語言的枚舉類型轉化為UCLID語言的枚舉類型；

指針類型轉化模塊，用于將Termite語言的指針類型轉化為UCLID語言的TERM類型的變量和參數為1的FUNC函數。

優選地，所述常數轉化模塊包括：

大常數轉化模塊，用于將Termite語言的大常數轉化為UCLID語言的CONST?TERM；

小常數轉化模塊，用于使用succ函數和pred函數對Termite語言的小常數進行處理。

優選地，所述操作命令轉化模塊包括：

TRUTH變量轉化模塊，用于使用布爾演算符操作將Termite語言的操作命令轉化為UCLID語言的TRUTH變量；

TERM變量轉化模塊，用于將Termite語言的操作命令轉化為UCLID語言的TERM變量。如果進行比較運算，則轉換成PRED函數，如果不進行比較運算，則轉換成FUNC函數。

優選地，所述一致性檢測模塊包括：變量添加模塊，用于在模型檢測工具中控制模塊的變量定義部分添加兩個變量，分別用于存儲由Termite代碼轉化的UCLID代碼執行預定狀態時所有寄存器的值，以及由Verilog代碼轉化的UCLID代碼轉移到上述狀態時所有寄存器的值。

優選地，所述一致性檢測模塊包括：匹配模塊，用于判斷兩變量存儲的所有寄存器的值是否完全相等。

(三)有益效果

本發明通過將設備規范語言和設備行為語言均轉化為模型檢測工具能夠識別的語言，并比較設備執行同一狀態情況下，設備規范語言和設備行為語言轉化為模型檢測工具的UCLID語言時設備所有寄存器變量的值，來檢測設備規范與設備行為的一致性，可以提高設備規范和設備驅動的可靠性。

附圖說明

圖1為本發明實施方式中所述設備規范與設備行為的一致性檢測系統的結構示意圖。

其中，1：設備規范轉化模塊，2：設備行為轉化模塊，3：一致性檢測模塊，4：變量轉化模塊，5：常數轉化模塊，6：操作命令轉化模塊，7：枚舉類型轉化模塊，8：指針類型轉化模塊，9：大常數轉化模塊，10：小常數轉化模塊，11：TRUTH變量轉化模塊，12：TERM變量轉化模塊，13：變量添加模塊，14：匹配模塊。

具體實施方式

下面結合附圖和實施例，對本發明的具體實施方式作進一步詳細描述。以下實施例用于說明本發明，但不用來限制本發明的范圍。

本發明所述的設備規范與設備行為的一致性檢測系統是基于一種設備規范與設備行為的一致性檢測方法提出的，該包括以下步驟：