[發明專利]一種基于AIG和SAT求解器的GSTE模型檢測方法

在審

• 申請號: 201310418675.3
• 申請日: 2013-09-14
• 公開（公告）號: CN103838908A
• 公開（公告）日: 2014-06-04
• 發明（設計）人: 楊國武;崔曉爽;高毅;康文濤;牛偉納;張艷;徐永生;楊俊;楊緒鵬;周志慧
• 申請（專利權）人: 電子科技大學
• 主分類號: G06F17/50
• 分類號: G06F17/50
• 代理公司: 成都華典專利事務所(普通合伙) 51223
• 代理人: 徐豐;楊保剛

1.一種基于AIG和SAT求解器的GSTE模型檢測方法，其特征在于包括以下步驟：

步驟1，使用ABC工具建立AIG模型；將該AIG轉化成FRAIG，同時使用邏輯綜合算法化簡該FRAIG，減小AIG規模；

步驟2，計算每條邊上的狀態集不動點Ψ*，在第一步中得到的AIG表示整個電路，也作為計算中使用的狀態遷移函數，不動點計算公式如下：

ψn+1(e)=ψn(e)∪(∪e-∈in(e)post(ψn(e-))∩ant(e))]]>

其中e表示邊，e-表示e的入邊，Ψ表示狀態集，使用FRAIG表示，ψ_n(e)表示當前已經計算出的存于邊上的狀態集合，ψ_n+1(e)表示下一步計算的狀態集合；Post()是狀態遷移函數，是給定一個狀態集和一個遷移關系，經過遷移后得到的狀態集；in(e)表示斷言圖中邊e的入邊，ant(e)表示邊上的ant狀態集，在下面出現的ψ_n^*(e)表示狀態集不動點，cons(e)表示邊上的cons狀態集；

步驟3：將算得的每條邊上的不動點和相應邊上的cons做驗證，若則報錯，并通過反向遷移找到反例；

步驟4：判斷每條邊上的狀態集是否到達不動點，若到達不動點，完成本次驗證，否則返回步驟2，進行下一輪狀態集的計算。

2.根據權利要求1所述的一種基于AIG和SAT求解器的GSTE模型檢測方法，其特征在于：所述步驟1中，建立AIG保存用于系統遷移關系和表示性質的斷言圖，斷言圖的一條邊用一個AIG表示，這些AIG具有相同名稱的輸出端口，并保持與遷移關系AIG的輸出端口不同名；

步驟1中初始建立的遷移關系的AIG是用多個等式的形式表示遷移關系，使用下面方法改造AIG，使其使用一個等式的形式表示遷移關系：

(1.1)一個AIG中每一個輸出端口和AIG網絡中的“與”節點表示一個等式關系，根據香農展開公式，改造當前AIG，將等式變成同或式，最終用一個輸出端口表示這些同或關系式；

(1.2)使用邏輯綜合算法對(1.1)中得到網絡化簡；

(1.3)使用ABC命令或者調用其內部函數，將(1.2)中得到的網絡轉化成FRAIG，同時對該FRAIG使用邏輯綜合命令化簡。