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

有效

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

本發明公開了一種基于SAT的電路錯誤診斷方法，首先將待診斷電路的網表結構、給定的觀測集共同轉化成CNF表達式，通過計算CNF表達式是否有解來判斷電路是否存在錯誤；如果電路存在錯誤，將電路的網表結構劃分成多個錯誤備選模塊，對每個錯誤備選模塊插入一個異或門組成的選擇電路，將原電路網表轉化成了診斷架構，然后提取該診斷架構的CNF表達式，對其進行SAT求解，根據解的形式判斷該錯誤備選模塊中是否有錯誤。本發明用基來簡化SAT求解，并將計算基過程中含有的大量多變元多項式除法運算轉化成乘法運算，從而加速基的計算過程。本發明能夠高效的診斷和定位電路中的錯誤、縮短芯片的功能驗證與調試時間。

技術領域

本發明屬于微電子領域中的VLSI芯片設計技術領域，具體涉及一種基于SAT的電路錯誤診斷方法。

背景技術

隨著超大規模集成電路(VLSI)設計工藝的發展，整個電子系統，比如386微處理機，都可以整合到一塊芯片上。VLSI電子設備具有體積小、可靠性高、功耗低等特點。但是隨著VLSI芯片整合的電路規模越來越大、電路設計越來越復雜，VLSI芯片的出錯率在增加、設計周期也在增長，而其中，電路的功能驗證與錯誤檢測大概占整個設計周期的60～70％。

一般來說，在VLSI芯片的設計初期，設計者使用硬件描述語言描述自己的設計思想，使用一系列的模塊來描述整個復雜的電路系統，此時電路設計處于行為級描述層次。然后，行為級描述要轉換成寄存器轉換級電路(RTL級電路)，描述數據在寄存器中的流轉狀況。最后，RTL級電路經過邏輯綜合得到門級電路。在電路的整個設計周期中，為了追求電路的效率和功能，可能需要不斷地對電路進行調整和優化：不論是為了優化效率而調整門電路實現，還是在修改了電路規范、電路功能后要對門電路進行調整。隨著VLSI電路的規模越來越大，結構越來越復雜，電路中引入錯誤的概率也越來越大。為了加快電路的功能驗證與錯誤檢測的速度、節約電路設計者的精力與時間，業界需要有效的電路錯誤診斷方法。

發明內容

本發明的目的在于克服現有技術的不足，提供一種基于SAT的電路錯誤診斷方法，能夠判斷電路是否存在錯誤，并定位電路錯誤位置。

本發明是通過以下技術方案實現的：

一種基于SAT的電路錯誤診斷方法，包括以下步驟：

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

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

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

步驟2：定位電路錯誤

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

在上述技術方案中，步驟1中，將待診斷電路的網表結構中的每個門電路，根據其真值表得到該門電路的CNF表達式；對于觀測集，根據其中各變量的取值得到對應的CNF表達式；將上述所有的CNF表達式進行與操作，得到最終完整的CNF表達式。

在上述技術方案中，步驟2中，如果診斷架構的CNF表達式有解，則錯誤備選模塊的輸出信號發生了反轉，說明該模塊產生了錯誤。

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