[發明專利]用于驗證電路的模型檢測中的模型抽象方法及其系統

有效

• 申請號: 200910083790.3
• 申請日: 2009-05-13
• 公開（公告）號: CN101556627A
• 公開（公告）日: 2009-10-14
• 發明（設計）人: 陳博文;沈海華
• 申請（專利權）人: 中國科學院計算技術研究所
• 主分類號: G06F17/50
• 分類號: G06F17/50
• 代理公司: 北京律誠同業知識產權代理有限公司
• 代理人: 祁建國;梁 揮

1.一種用于驗證電路的模型檢測中的模型抽象方法，所述電路為 Verilog設計，其特征在于，所述方法包括：

步驟1，讀入所述電路的Verilog代碼，依據檢測需求處理所述Verilog 代碼中的變量，以規范并簡化所述代碼；所述步驟1進一步為，

步驟21，讀入所述電路的Verilog代碼，將所述代碼轉化為規范形式， 所述規范形式中代碼的一個模塊包括變量聲明和賦值語句；

步驟22，獲得以所述檢測需求為依據的數據字及所述數據字對應的抽象 域，將所述變量聲明中的變量中未被定義為數據字的部分中每個比特作為邏 輯個體的數據位；其中，所述數據字是邏輯上作為整體的比特序列；所述抽 象域是一個名字的序列；

步驟23，對所述數據字和所述數據位分別生成新的變量，分別對應為字 變量和位變量，將所述賦值語句中的變量引用，依據數據字與字變量的比特 對應關系或者數據位與位變量的比特對應關系替換為對所述字變量或位變量 的引用，刪除所述變量聲明；

步驟24，從所述賦值語句中提取對變量賦值的賦值表達式，并刪除所述 賦值語句；

步驟2，根據規范后的所述變量和所述變量的賦值，提取所述電路的數 據路徑；具體包括下列步驟，

步驟71，處理所述變量的賦值表達式，標記出字傳遞表達式以及字傳遞 網線變量，刪除所有字傳遞網線變量；

步驟72，對變量進行選擇傳遞；

步驟3，提取所述數據路徑的數據運算，根據所述數據運算抽象所述數 據路徑；所述步驟3進一步為，

步驟121，提取出所述電路中對于數據字的兩種運算，一種運算為所述 電路的控制部分在數據流中提取信息，另一種運算為所述電路對數據字進行 運算并生成數據；

步驟122，根據所述數據字對應的抽象域，生成抽象變量，并抽象所述 兩種運算；其中，所述抽象變量是對原始變量的值域進行抽象后生成的變量；

步驟4，對抽象后的所述代碼中的變量和所述變量的賦值進行操作，生 成自動機的狀態集合和邊集合，具體包括：

生成狀態集表達式和邊集表達式。

2.如權利要求1所述的用于驗證電路的模型檢測中的模型抽象方法，其 特征在于，所述數據字滿足的條件包括：

數據字為一個變量引用或者為多個變量引用的連接；

數據字只引用輸入變量、輸出變量和寄存器變量；

在數據字為多個變量引用的連接時，該變量引用所引用的變量的類型相 同；所述類型包括：輸入、輸出或寄存器；

數據字包含至少兩個比特；

所有數據字中任意兩個變量的任一比特在整個數據字定義中最多只出現 一次。

3.如權利要求1所述的用于驗證電路的模型檢測中的模型抽象方法，其 特征在于，所述步驟22中將變量中未被定義為數據字的部分中每個比特作為 邏輯個體的數據位進一步為，

步驟41，對于每個輸入變量、輸出變量和寄存器變量中的一個比特，如 果所述比特未被包含在任何所述數據字中，則所述比特為一個所述數據位。

4.如權利要求1所述的用于驗證電路的模型檢測中的模型抽象方法，其 特征在于，

所述步驟23還包括字變量和位變量繼承定義所述數據字和數據位的變 量的類型，

所述類型包括：輸入、輸出和寄存器。

5.如權利要求1所述的用于驗證電路的模型檢測中的模型抽象方法，其 特征在于，

所述步驟24中變量的類型包括：輸出、寄存器和網線。