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

無效

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

1.一種設備規范與設備行為的一致性檢測系統，其特征在于，包括：

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

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

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

2.如權利要求1所述的設備規范與設備行為的一致性檢測系統，其特征在于，所述設備規范轉化模塊(1)包括：

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

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

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

3.如權利要求2所述的設備規范與設備行為的一致性檢測系統，其特征在于，所述變量轉化模塊(4)包括：

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

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

4.如權利要求2所述的設備規范與設備行為的一致性檢測系統，其特征在于，所述常數轉化模塊(5)包括：

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

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

5.如權利要求2所述的設備規范與設備行為的一致性檢測系統，其特征在于，所述操作命令轉化模塊(6)包括：

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

TERM變量轉化模塊(12)，用于將Termite語言的操作命令轉化為UCLID語言的TERM變量。

6.如權利要求1所述的設備規范與設備行為的一致性檢測系統，其特征在于，所述一致性檢測模塊(3)包括：變量添加模塊(13)，用于在模型檢測工具中控制模塊的變量定義部分添加兩個變量，分別用于存儲由Termite代碼轉化的UCLID代碼執行預定狀態時所有寄存器的值，以及由Verilog代碼轉化的UCLID代碼轉移到上述狀態時所有寄存器的值。

7.如權利要求6所述的設備規范與設備行為的一致性檢測系統，其特征在于，所述一致性檢測模塊(3)包括：匹配模塊(14)，用于判斷兩變量存儲的所有寄存器的值是否完全相等。