[發明專利]一種基于SAT的電路錯誤診斷方法

有效

• 申請號: 202110202215.1
• 申請日: 2021-02-24
• 公開（公告）號: CN112836456B
• 公開（公告）日: 2022-11-15
• 發明（設計）人: 蘇明;王燦燦;王剛;張青坡
• 申請（專利權）人: 南開大學
• 主分類號: G06F30/3315
• 分類號: G06F30/3315
• 代理公司: 天津創智睿誠知識產權代理有限公司 12251
• 代理人: 王海濱;田陽

1.一種基于SAT的電路錯誤診斷方法，其特征在于，包括以下步驟：

步驟1，判斷電路是否存在錯誤；

步驟1.1：將待診斷電路的網表結構、給定的觀測集共同轉化成CNF表達式；

步驟1.2：計算是否存在使得上述CNF表達式為真的解，將判斷電路是否存在錯誤問題轉化為SAT求解問題；若上述CNF表達式無解，則電路存在錯誤；

步驟2：定位電路錯誤；

將電路的網表結構劃分成多個錯誤備選模塊，對每個錯誤備選模塊，在該模塊的輸出信號后插入一個異或門組成的選擇電路，記插入的選擇電路的選擇信號為s，將原電路網表轉化成了診斷架構；然后提取該診斷架構的CNF表達式，該表達式是將診斷架構中的每個門電路的CNF式子相與得到的；對CNF表達式進行SAT求解，根據所得解的形式判斷該錯誤備選模塊中是否有錯誤；

利用基來簡化SAT求解，具體步驟包括：將CNF表達式按照與運算拆分成多個較為簡短的布爾表達式；將拆分后的各個布爾表達式轉化成GF(2)上的多變元多項式，分別記為f₁,…,f_m，計算CNF表達式的可滿足性解等價于計算下述多元多項式方程組(1)的解，方程組(1)表達式為：

計算理想I＝f₁+1,…,f_m+1的基G＝{g₁,…,g_M}；方程組(1)等價于下述方程組(2)，方程組(2)表達式為：

接下來計算多元多項式方程組(2)的解，所得解即為CNF表達式的可滿足性解；

利用Buchberger算法計算理想I＝f₁+1,…,f_m+1的基G＝{g₁,…,g_M}；Buchberger算法如下：

輸入：F＝{f₁,f₂,…f_m}，項序；

輸出：G＝{g₁,…,g_M}，G是理想f₁,f₂,…f_m的基；

初始化：G＝F,DF＝{{f_i,f_j}|f_i≠f_j,f_i,f_j∈G}；

當作：

選擇{f,g}∈DF，DF：＝DF\{{f,g}}，

r相對于G是既約的，

如果r≠0，則：

G：＝G∪{r}，

其中步驟就是計算多項式S(f,g)除以G中多項式的余多項式，多元多項式的除法算法如下：

輸入：f,F＝{f₁,f₂,…f_m}，項序；

輸出：r,u₁,…,u_m，使得：

r相對F是既約的；

初始化：u₁：＝0,u₂：＝0,…,_m∶＝0,r:＝0,h:＝f；

當h≠0，作：

如果使得lp(f_i)|lp(h)，則選擇具此性質的最小i，令：

否則：

r：＝r+lt(h)，

h：＝h-lt(h)，

為了提高計算效率，針對GF(2)上的多元多項式每次除法運算，將其轉換成一次乘法運算：記要計算的多元多項式除法為f’/g’；選定項序為字典序；記f’除以g’的商多項式為q，余多項式為r，即f’＝qg’+r；記g’中首項為lt(g’)，記集合S為f’中能被lt(g’)整除的子項的集合，則有：

r＝f′-qg′，

進而，多元多項式的除法運算f’/g’轉換成一次乘法qg’運算；

針對轉化后的GF(2)上多元多項式乘法qg’運算，采用karatsuba算法進行快速乘法運算。