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

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

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

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

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

在電路的形式化驗(yàn)證方面，形式化驗(yàn)證工具主要有兩類：模型檢測(cè)工具和等價(jià)性驗(yàn)證工具。模型檢測(cè)主要是用來(lái)證明一個(gè)電路是否滿足某個(gè)屬性，而等價(jià)性驗(yàn)證用來(lái)證明兩個(gè)電路是否等價(jià)。

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

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

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

SAT 涉及到的基本概念包括變量、文字、子句（子句是文字的析?。⒑先》妒剑ê?jiǎn)稱CNF，子句的合取，即子句集合）。SAT 的求解一般采用合取范式輸入，也有針對(duì)電路的 SAT 問(wèn)題。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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