[[441194]]

本文轉(zhuǎn)自雷鋒網(wǎng)，如需轉(zhuǎn)載請至雷鋒網(wǎng)官網(wǎng)申請授權(quán)。

2021 年 12 月 9 日-2021 年 12 月 11 日，2021 第六屆全球人工智能大會（GAIR 2021）于深圳正式召開。歷經(jīng)五年，見證數(shù)次潮水的轉(zhuǎn)向，成為目前為止粵港澳大灣區(qū)人工智能領(lǐng)域規(guī)模最大、規(guī)格最高的學(xué)術(shù)、工業(yè)和投資領(lǐng)域跨界盛會。

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

EDA是中國芯片產(chǎn)業(yè)發(fā)展的卡脖子技術(shù)，求解器又是EDA的基礎(chǔ)引擎，解決了基礎(chǔ)技術(shù)挑戰(zhàn)才能支撐整個產(chǎn)業(yè)的快速發(fā)展——基于此，中國科學(xué)院軟件研究所研究員蔡少偉主要從自己的研究角度談到了 EDA 的發(fā)展。

蔡少偉的演講主要涵蓋三個方面，一是 EDA 和 SAT 求解器的關(guān)系；二是舉例說明 SAT 求解器在 EDA 當(dāng)中的應(yīng)用；三是分享其團(tuán)隊在 SAT 求解器方面的進(jìn)展。

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

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

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

以下是蔡少偉在GAIR 2021 上的演講內(nèi)容，雷峰網(wǎng)(公眾號：雷峰網(wǎng))進(jìn)行不改變原意的編輯整理：

今天的匯報分為3個部分：一是 EDA 和 SAT 求解器的關(guān)系；二是舉幾個例子說明 SAT 求解器在 EDA 中的應(yīng)用；三是介紹團(tuán)隊在 SAT 求解器方面的進(jìn)展。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

在電路測試?yán)铮m然設(shè)計過程已經(jīng)比較準(zhǔn)確，但實際上，芯片生產(chǎn)和設(shè)計不一定一致，生產(chǎn)過程中存在一些不確定因素，比如雜質(zhì)的污染導(dǎo)致某條路線、電路路線短路或是斷路，會造成芯片與原來設(shè)計的不一樣。電路測試要做的是盡量覆蓋缺陷模型，不會出現(xiàn)類似錯誤。我們要做的，是產(chǎn)生一組輸入向量，覆蓋測試的缺陷。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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