中國科學院研究員蔡少偉：SAT 求解器 EDA 基礎引擎 | GAIR 2021

雷峰網(公眾號：雷峰網)按：2021 年 12 月 9 日-2021 年 12 月 11 日，2021 第六屆全球人工智能大會（GAIR 2021）于深圳正式召開。歷經五年，見證數次潮水的轉向，成為目前為止粵港澳大灣區人工智能領域規模最大、規格最高的學術、工業和投資領域跨界盛會。

在大會第二天舉辦的“集成電路高峰論壇：國產高端芯片之路”上，匯聚來自學術界、產業界和投資界的 15 位大咖，共同探討了國產高端芯片的實力以及 RISC-V 帶給中國芯片的機會。

EDA是中國芯片產業發展的卡脖子技術，求解器又是EDA的基礎引擎，解決了基礎技術挑戰才能支撐整個產業的快速發展——基于此，中國科學院軟件研究所研究員蔡少偉主要從自己的研究角度談到了 EDA 的發展。

蔡少偉的演講主要涵蓋三個方面，一是 EDA 和 SAT 求解器的關系；二是舉例說明 SAT 求解器在 EDA 當中的應用；三是分享其團隊在 SAT 求解器方面的進展。

蔡少偉表示，EDA 集成電路設計自動化軟件，整條鏈很長，而不是單個的軟件。在 EDA 軟件中，其底層需要一些計算引擎，而主要的計算引擎就是 SAT 求解器。

在 EDA 各個環節中，包括邏輯綜合、物理實現，以及中間的驗證、仿真測試都會用到 SAT 求解器。

目前，蔡少偉團隊的 SAT 求解器已經用于集成電路驗證的實際場景，在 1 小時內可求解出一些近 2 億子句規模的算例。

以下是蔡少偉在GAIR 2021 上的演講內容，雷峰網進行不改變原意的編輯整理：

今天的匯報分為3個部分：一是 EDA 和 SAT 求解器的關系；二是舉幾個例子說明 SAT 求解器在 EDA 中的應用；三是介紹團隊在 SAT 求解器方面的進展。

EDA 的全稱是 Electronic  Design  Automation，是指集成電路的設計自動化軟件，用這樣一套軟件自動設計集成電路，一般都稱 EDA 為芯片之母，是整個半導體的最上游、支撐芯片乃至整個信息產業的共性基礎技術。

 EDA集成電路設計自動化軟件不是單個的軟件，整個條鏈很長，我們可以把 EDA 軟件當成硬件編譯器，用硬件描述語言寫出芯片的需求，通過 EDA 軟件可以幫助我們自動的設計出芯片集成電路的版圖。

EDA 軟件里面，底層需要一些計算引擎，而主要的計算引擎就是 SAT 求解器，在 EDA 的各個環節里，包括邏輯綜合、物理實現，以及中間的驗證、仿真測試其實都要用到 SAT 求解器。

比如，以邏輯綜合為例，在邏輯綜合的歷史上，SAT 求解器一直扮演非常重要的角色，尤其是在邏輯綜合的發展史上最后一個階段，優化和表示都要極大依賴 SAT 求解器。

在電路的形式化驗證方面，形式化驗證工具主要有兩類：模型檢測工具和等價性驗證工具。模型檢測主要是用來證明一個電路是否滿足某個屬性，而等價性驗證用來證明兩個電路是否等價。

以模型檢測技術的發展為例，在這個發展歷史階段中，從 2000 年之后開始的模型檢測技術基本都是基于 SAT 求解器來開發的。

通常情況下，計算機解決問題的時候有兩類思路：一是把問題清楚地用數學語言描述出來，再設計算法求解，這是約束求解的思路，典型場景包括定理證明等。二是機器學習，用戶提供例子，計算機解決問題，比如，各種模式識別的任務比較適用于機器學習。對于需要嚴格證明的場景，則需要約束求解來解決。

SAT 的全稱是布爾可滿足性問題，這個問題的描述非常簡單，即給定一個布爾公式或稱為命題邏輯公式，也即用與或非等邏輯連接詞連接起來的公式，判斷是否能給公式里的變量賦值使得公式為真。如果存在這樣的賦值，就說這個公式是可滿足的，否則就是不可滿足的。

SAT 涉及到的基本概念包括變量、文字、子句（子句是文字的析?。?、合取范式（簡稱CNF，子句的合取，即子句集合）。SAT 的求解一般采用合取范式輸入，也有針對電路的 SAT 問題。

關于 SAT 在 EDA 中的典型應用，為了把 SAT 求解電路中的問題，首先得把電路轉為 SAT 可以接受的輸入形式。其中，將電路轉為 CNF 有比較簡單的編碼方式，有線性時間和線性規模，相對比較方便。

表格左邊是電路的邏輯門，右邊是對應的 SAT 公式。這樣，電路就可以轉為合取范式，成為 SAT 的輸入形式。

剛剛已經理解的電路可以轉為 SAT 公式，那么，如何在多數 EDA 場景中利用 SAT 求解器呢？我們舉幾個例子：

首先看模型檢測工具，模型檢測工具是要檢測一個電路是否滿足某個屬性，比如“寄存器肯定不會有沖突”。我們需要用自動機模型把刻劃出電路行為，而驗證的屬性用時序邏輯相關的公式表達。要證明這個模型是否能蘊含屬性，也就是在這個模型下的屬性是否成立，這個就叫模型檢測。這個任務的核心需要調用 SAT 求解器。

這是一個計數器的例子，我們拿到硬件描述源 Verilog 模塊，將從第一位跳到 第2、3位，然后再重啟。對Verilog 模塊進行編譯，得到一個網表，包括計存器、網門的邏輯門連接，最后可以得到這個網表對應的狀態轉移模型，也就是自動機模型。

有了這個模型之后，還要得到驗證屬性對應的公式。有界模型檢測是檢測 K 步（K 是給定）之內是否存在一條路徑。前面提到，是否存在一條路徑走完 K 步后會違反指定屬性呢？這就是為什么我們需要把屬性翻譯成邏輯公式。

我們關心兩類屬性，一類是 Safety 屬性，指壞的事情永遠不會發生，是用全局的時序詞Gp 表示，p 就是要滿足的屬性。將公式寫出來，用自然語言先理解一下，如果存在一條路徑初始狀態可以達到某個狀態，這個狀態使得 p 不成立，我們就找到一個反例。如果不存在這樣的路徑，說明 Gp 在 k 步之內肯定是成立的。

另一個是 Liveness 屬性，是指好的事情終會發生，用 Fp  表示。同樣，我們考慮的還是它的反面：假如這個公式不成立，對應有一段路徑跟著一個循環，并且這個路徑上任何狀態下 p 都不成立，因此這個屬性就不滿足了。

結合前面所說，可以講將其翻譯成一條 SAT 公式，如果這條公式用 SAT 求解器來判定，它是可滿足的，就意味著它存在一個反例，并且可以對應地將這條反例構造出來。如果這個公式是不可滿足的，就是說不存在反例，這個屬性是被驗證滿足的了。

形式化驗證的第二類是等價性驗證。兩個電路等價，就是說在任何輸入的情況下兩個電路的輸出都一樣，在功能上是等價的。那么，這個事情用 SAT 怎么做呢？

首先，可以先考慮單輸出的，將兩個電路 N1、N2 的輸出通過異或門連接，如果能夠找到一組輸入使得異或門的輸出是1，意味著 N1 和 N2 兩個電路的輸出是不一樣的，即不等價。如果找不到這樣的輸入，則意味著是等價的。

如果有多輸出電路也是一樣，把每個對應的輸出 N1、N2 對應的輸出做異或，最后做一個或門連接起來。使得最后的門輸出為 1，意味著這些輸出肯定有一對是不相等的，所以是不等價。

這個流程可以用 SAT 求解器做出來，構造混合電路后變成 CNF 公式，即 SAT 的輸入形式。如果能找到這個公式的解，也就是找到反例，說明是不等價的。反之，如果可以證明這一對應的公式是不可滿足的，也就說明這兩個電路是等價的，這就是等價性驗證目前的技術。

除了形式化驗證，在邏輯綜合里有很多應用，比如電路結構的優化，找到某個子結構進行替換，在確保替換正確的情況下，要做一些 SAT 去查詢兩個結構是否可以替換。

在電路測試里，雖然設計過程已經比較準確，但實際上，芯片生產和設計不一定一致，生產過程中存在一些不確定因素，比如雜質的污染導致某條路線、電路路線短路或是斷路，會造成芯片與原來設計的不一樣。電路測試要做的是盡量覆蓋缺陷模型，不會出現類似錯誤。我們要做的，是產生一組輸入向量，覆蓋測試的缺陷。

一個常見的缺陷被稱為 stuck-at fault，關注路線是不是短路或是斷路；此外還有延遲缺陷模型。

如果一條線在我們不知情的情況下斷了，得通過測試找出來，只有這條線斷了后輸出的情況和沒斷的情況不一樣，才能發現異常。一個電路要測試 stuck-at fault，要覆蓋兩倍電路線數量的缺陷。

比如說，這是三位乘二位的乘法，對應的電路有 50 條線，要檢測100 個潛在的  stuck-at fault，非常樸素的做法就是把所有可能的輸入和實際輸出和設計的電路所期待的輸出對比是不是一樣，不一樣就找到一些錯誤。雖然可以百分之百的覆蓋，但太低效，目前產業界不可能做類似枚舉。

ATPG 就是利用 SAT 求解器用盡可能少的輸入覆蓋盡可能多的錯誤，一般情況下，第一步會隨機產生一些輸入向量，覆蓋大部分要關注的錯誤，剩下的即是比較難能隨機覆蓋的，需要通過對應的 SAT 求解器求出可以覆蓋對應的 input 向量，最終壓縮產生 Bachmark。

如圖，假設 d 這條線斷了，它為 0，要找到一個輸入使得正常設計的情況下輸出和在另一邊輸出不一樣，從而發現出現斷路的情況。

由此，要產生一個滿足兩個條件的測試向量：一是錯誤的激活，二是錯誤要傳播，將兩個條件編碼為一個 CNF 公式，合起來其實也是 SAT 求解問題。

SAT 求解器在 EDA 中如此重要，那么，它目前做得怎么樣？

SAT 是一個邏輯問題，很容易會采用邏輯推理的方法思考，比如說歸結原理。但把它看作在搜索空間找賦值，判斷它是否存在合法的解，因此搜索的方法也可行。

SAT 求解方法可以分為兩類：完備算法和不完備算法。完備算法是指算法只要給足時間，肯定會產生正確答案，Yes  or  No，但這個時間在理論上沒有保證；不完備算法是指爭取短時間內找到解。

SAT 求解器非常重要，在歷史上有很多科學家在研究，完備算法從 1960 年開始有了，不完備算法從 1992 年開始。其中，最重要的是 1996 年 CDCL，它的一個break  through。

歷史上，1997 年 Bart Selman 提出命題邏輯推理十個挑戰，其中第七個是能否結合產生更 powerful 的方法，這是我們近期研究的方向。

以前的方法是側重于系統搜索和局部搜索，這兩個方法求解能力互補，即使采用并集，實際上在工業上沒有得到改進，原來的方法不能求解，通過并集的方法也求解不了。

近期，我們基于完備搜索進行求解，把隨機搜索的不完備方法當成采樣工具，采樣的信息幫助完備算法求解，基于信息交互的深度合作。在過去幾年比賽的工業實例上，這一方法產生的混合算法可以求解原來兩個算法都不能求解的算例，比例達到 12% ，達到了工業實例上的顯著改進，首次回答了這一挑戰。

同時，這一方法也直接用到實際場景的集成電路驗證，可以求解達到近 2 億子集的1小時求解規模。

在今年的 EDA 比賽，我們拿到全球第二名的好成績，這說明做好 SAT 求解器對 EDA 十分重要，相關的方法已發表在SAT 2021，獲得最佳論文獎。

總結：SAT 求解器作為 EDA 關鍵引擎起到重要的作用，這方面的重要進展目前是混合求解的方法取得突破。謝謝大家。

雷峰網原創文章，未經授權禁止轉載。詳情見轉載須知。