基于布爾可滿足性的精確邏輯綜合綜述

儲著飛 潘鴻洋

(寧波大學(xué)信息科學(xué)與工程學(xué)院 寧波 315211)

1 引言

電子設(shè)計自動化(Electronic Design Automation, EDA)工具及其設(shè)計方法學(xué)是集成電路(芯片)設(shè)計的核心，EDA工具通過提供自動化設(shè)計過程幫助芯片設(shè)計師設(shè)計開發(fā)，主要分為前端設(shè)計和后端設(shè)計，其中，邏輯綜合與優(yōu)化是現(xiàn)代EDA流程中的關(guān)鍵組成部分，屬于前端設(shè)計的核心。邏輯綜合是將用戶設(shè)計的數(shù)字電路轉(zhuǎn)換為工藝庫網(wǎng)表的過程，輸入通常是寄存器傳輸級硬件描述語言(Register Transfer Level, RTL)、工藝庫文件和設(shè)計約束文件，經(jīng)過翻譯、邏輯優(yōu)化和工藝映射等步驟輸出工藝庫網(wǎng)表。綜合出的網(wǎng)表質(zhì)量直接影響到后續(xù)的物理設(shè)計過程。

邏輯優(yōu)化以邏輯表達為基礎(chǔ)，在邏輯功能一致的前提下優(yōu)化邏輯表達的邏輯深度、開關(guān)活動性、文字數(shù)(literals)或節(jié)點個數(shù)等，分別對應(yīng)具體工藝下的性能(Performance)、功耗(Power)和面積(Area)，即PPA優(yōu)化。傳統(tǒng)邏輯優(yōu)化算法從其數(shù)學(xué)基礎(chǔ)分類主要分為代數(shù)法和布爾法，其中代數(shù)法又稱為多項式代數(shù)法，基于普通代數(shù)發(fā)展而來；布爾法則充分利用布爾代數(shù)區(qū)別于普通代數(shù)的特性，增強了對布爾空間的搜索能力。從算法尋優(yōu)能力分類又可分為啟發(fā)式算法和最優(yōu)算法，前者用可接受的成本計算出一個次優(yōu)解，而后者則不惜成本找到問題的最優(yōu)解。超大規(guī)模數(shù)字集成電路在邏輯優(yōu)化中因受制于規(guī)模約束，常采用全局啟發(fā)式，局部最優(yōu)算法的模式。在邏輯綜合中，基于最優(yōu)算法尋找最優(yōu)邏輯表達式的過程稱為精確邏輯綜合(exact synthesis)，最優(yōu)綜合和精確綜合?；Q使用[1]。最優(yōu)邏輯表達式指的是布爾邏輯函數(shù)的邏輯表達用到的節(jié)點數(shù)最少或者邏輯深度最小等。隨著算力的提升，邏輯優(yōu)化越來越追求最優(yōu)解而不滿足于次優(yōu)解。

精確綜合采用的最優(yōu)算法常通過約束求解器完成決策，常用的求解器包括定理證明器、整數(shù)線性規(guī)劃求解器、布爾可滿足性(Boolean SATisfiability,SAT)求解器、可滿足性模理論(Satisfiability Modulo Theory, SMT)求解器等。精確綜合得到的結(jié)果可用于大規(guī)模數(shù)字電路的局部優(yōu)化以及新興計算范式的設(shè)計，提升了綜合優(yōu)化的結(jié)果質(zhì)量(quality of result)。因SAT求解器及其算法的發(fā)展，近年來基于SAT編碼及求解的精確綜合受到廣泛關(guān)注，對專用集成電路(Application Specific Integrated Circuit, ASIC)和現(xiàn)場可編程門陣列(Field Programmable Gate Array, FPGA)，以及新興計算范式如存算一體系統(tǒng)、近似計算、隨機計算等帶來新的優(yōu)化機會。

本文對精確綜合的SAT編碼問題以及對應(yīng)的精確綜合應(yīng)用進行綜述，首先對邏輯函數(shù)的表達方式和布爾可滿足性問題等背景知識進行介紹；第3節(jié)針對精確綜合算法進行具體闡述；第4節(jié)歸納總結(jié)了目前國內(nèi)外常見的基于布爾可滿足性的精確綜合使用場景；最后探討了研究挑戰(zhàn)和未來發(fā)展趨勢。

2 背景

本節(jié)首先介紹邏輯函數(shù)的表達方式，然后介紹SAT問題及常用的算法。

2.1 邏輯表示

如何表示邏輯函數(shù)是邏輯綜合首先面臨的問題，邏輯函數(shù)從早期的真值表/卡諾圖，到“積之和(Sum Of Products, SOPs)”、2元決策圖(Binary Decision Diagram, BDD)、發(fā)展到如今的有向無環(huán)圖(Directed Acyclic Graph, DAG)，其可表達和處理的邏輯函數(shù)規(guī)模逐漸增大。

布爾鏈(Boolean chain)是DAG的一種，每個頂點有k個輸入，執(zhí)行k元邏輯運算。布爾鏈概念提出時k=2[2]，但k可推廣到任意大的有限數(shù)，且一個布爾鏈中的k是唯一的[3]。其形式化定義如下，給定一個m輸出的函數(shù)f={f1,f2,...,fm}，每個輸出函數(shù)的輸入屬于集合{x1,x2,...,xn}，那么這些函數(shù)的布爾鏈可表示成一個r步(驟)序列(xn+1,xn+2,...,xn+r)，序列中每一步的輸入都是前序已計算的步驟。以k=2為例

且f1=x4,f2=x5。因 此l(1)=4,l(2)=5。其DAG圖形化示意圖如圖1所示，其中‘∧’為與門，f={f1,f2}={x1x2,x1x2⊕x3}。

圖1 布爾鏈?zhǔn)疽鈭D

此外，邏輯綜合中常用的D A G 還有A I G(AND-Inverter Graph,), MIG (Majority-Inverter Graph)等。其中AIG與布爾鏈的區(qū)別是每個內(nèi)部節(jié)點只能實現(xiàn)2輸入‘與’操作，而連接邊包含原邊和補邊，補邊表示反相器運算；MIG則是對AIG的推廣，每個內(nèi)部節(jié)點實現(xiàn)的是3輸入“多數(shù)邏輯門”(majority-of-three)。因此，通過限定布爾鏈的輸入k以及內(nèi)部節(jié)點的邏輯功能，會衍生出不同的基于DAG的邏輯表示。

2.2 SAT問題

SAT問題是著名的判定問題，給定描述問題的布爾公式，判定是否存在1組或多組變量的取值組合，能夠使布爾公式取值為真，如果存在使布爾公式取值為真的變量取值組合，稱該布爾公式是可滿足的(SAT)，否則該布爾公式是不可滿足的(UNSAT)。一個布爾變量或者其反變量稱為文字，若干文字的析取式又稱為子句(clause)，所有子句的合取式則構(gòu)成了描述問題的布爾公式，即合取范式(Conjunction Normal Form, CNF)。

以x2(x1∨xˉ2∨x3)(xˉ1∨x3)為例，該CNF包含3個子句，分別是x2,(x1∨xˉ2∨x3), (xˉ1∨x3)，其中x2是單文字子句，要使該CNF為真，則每個子句必須為真，此例中x2只有賦值為真才能滿足約束。經(jīng)過推理，x3為 真，x1任意賦值即可使CNF為真。將問題轉(zhuǎn)換為CNF描述的過程稱為SAT編碼，求解CNF的過程稱為SAT求解算法，給定CNF輸入獲得SAT判定結(jié)果的工具又稱為SAT求解器。可見SAT求解器的核心是對CNF的處理和求解算法，一般問題通過SAT編碼調(diào)用現(xiàn)成的SAT求解器即可獲得結(jié)果，因此很多SAT求解器的應(yīng)用難點在于如何將問題進行高效的SAT編碼。

SAT問題還有很多變種，比如k-SAT問題限定子句中的文字數(shù)不超過k，最大SAT(max-SAT)則努力找到一個能滿足最多子句的賦值，全解SAT(all-SAT)則需要找到所有可能的賦值。較常見的SAT求解器包括 Chaff, MiniSAT等。

3 精確綜合

相比于基于啟發(fā)式算法的邏輯綜合，精確邏輯綜合的研究則要少得多，其中最難突破的問題就是計算的復(fù)雜度高，需要依靠枚舉完成推理和決策。奎因-麥克拉斯基(Quine-McCluskey)算法是知名的2級邏輯SOP最小化算法[4]， 因受制于計算復(fù)雜度，后來發(fā)展的啟發(fā)式優(yōu)化方法Espresso更受歡迎。精確綜合需要給定1個或者1組布爾邏輯函數(shù)F、用來表示邏輯函數(shù)的邏輯門集合/邏輯原語集合L以及成本函數(shù)C。

從精確綜合所采用的方法來看，傳統(tǒng)的精確綜合包含以下3種方式[5]。

(2) 給定邏輯操作符號集合L， 由n個邏輯門組成的邏輯網(wǎng)絡(luò)個數(shù)是有限的，通過枚舉邏輯網(wǎng)絡(luò)，并對邏輯網(wǎng)絡(luò)節(jié)點賦操作符，可得到不同的邏輯函數(shù)，得到的邏輯函數(shù)與綜合的邏輯函數(shù)進行比對，如果一致則找到最優(yōu)解，否則增大n進入下一次枚舉。n從0開始，顯然，隨著n增大所枚舉的邏輯網(wǎng)絡(luò)個數(shù)非線性增長。

(3) 結(jié)合第(1)和第(2)種方法同時進行函數(shù)分解和邏輯網(wǎng)絡(luò)枚舉的混合方式尋優(yōu)。

然而，這些方法所能處理的邏輯函數(shù)規(guī)模非常有限，只能通過枚舉來證明最優(yōu)性。近年來，隨著算力的提高以及理論計算機科學(xué)的發(fā)展，利用約束求解器，特別是SAT求解器進行決策和判定的精確綜合方法受到廣泛關(guān)注。基于SAT的精確綜合在2007年計算機輔助設(shè)計中的形式化方法(Formal Methods in Computer-Aided Design, FMCAD)會議上由MiniSAT作者Eén[6]提出。隨后，Knuth[2]使用了不同的CNF編碼進行精確綜合，但僅限于2輸入算子最優(yōu)布爾鏈計算，這些算法都旨在找到面積最優(yōu)(布爾鏈節(jié)點數(shù)最少)的布爾鏈。Soeken等人[7]將它們擴展到綜合邏輯深度最優(yōu)的布爾鏈，使用SAT求解器來檢查是否存在約束下實現(xiàn)給定功能的最少邏輯層級的布爾邏輯網(wǎng)絡(luò)。故基于SAT的精確綜合的任務(wù)是在大小或深度方面為給定的輸入約束找到最優(yōu)邏輯表達。

3.1 精確綜合算法流程

圖2(a)所示為求解最優(yōu)面積的精確綜合算法流程圖，核心思想是通過約束編碼并調(diào)用求解器回答問題“是否存在r個屬于集合L的邏輯門構(gòu)成的邏輯網(wǎng)絡(luò)實現(xiàn)待綜合的布爾函數(shù)集合F?”，成本函數(shù)C=r。因此r的初值為0，這主要是考慮到一些待綜合的函數(shù)是常數(shù)0或1、原始輸入(primary input)或者其反變量等，此時不需要邏輯門，例如F={1,x1}，x1為原始輸入，則待綜合的函數(shù)就是不需要邏輯門的簡單情況。在給定的r變量約束下通過產(chǎn)生基于CNF的SAT編碼F?，并將其交給SAT求解器計算，若SAT求解器返回可滿足解，則找到了實現(xiàn)待綜合函數(shù)的最優(yōu)邏輯網(wǎng)絡(luò)；否則將r增1，并再次編碼求解指導(dǎo)SAT返回可滿足解。因此能確保得到結(jié)果是最優(yōu)的，即用最少邏輯門實現(xiàn)待綜合邏輯函數(shù)。給定r的上界或者限定SAT求解器的時間都能使算法提前終止。

從算法的流程看出，在r變量和邏輯門集合L的約束下進行SAT編碼是最重要的步驟。此外，算法的復(fù)雜度與r的大小密切相關(guān)，當(dāng)r較小時，SAT編碼的變量個數(shù)和子句個數(shù)相對較少，因此SAT求解器往往能快速返回結(jié)果；如果一個函數(shù)很復(fù)雜，需要較多的r個邏輯門才能實現(xiàn)，顯然SAT求解器的求解難度會隨著SAT編碼變量的個數(shù)以及子句個數(shù)增加而增大，例如假定最優(yōu)解r=10，那么在r=0～9的自底向上遞增過程中SAT都在努力證明這些F?是不滿足的(UNSAT)。

相比于自底向上增加r引起的無效搜索，文獻[8]提出了自頂向下降低r的綜合流程如圖2(b)所示。首先通過函數(shù)分解獲得待綜合函數(shù)節(jié)點個數(shù)上界r，嘗試調(diào)用SAT求解器回答問題“是否存在r=r-1個屬于集合L的邏輯門構(gòu)成的邏輯網(wǎng)絡(luò)實現(xiàn)待綜合的布爾函數(shù)集合F?”，如果是不滿足的，則說明r+1 已經(jīng)是最優(yōu)值；否則繼續(xù)減小r直到SAT求解器返回UNSAT。同理，如何獲得一個較為緊湊的r上界至關(guān)重要。

圖2 基于SAT的精確綜合流程圖

3.2 SAT編碼

(1) 變量定義。若待綜合的邏輯函數(shù)原始輸入數(shù)為n，原始輸出數(shù)為m，當(dāng)前待編碼的邏輯門個數(shù)是r， 對于1≤h ≤m,n＜i ≤n+r， 且0＜t ＜2n，分別定義如下布爾變量：

(a)xit， 表示邏輯門xi真 值表的第t位。

(b)ghi， 表示邏輯門xi是 邏輯函數(shù)的第h個輸出。

(c)sijk，表示邏輯門xi的輸入是xj和xk，其中1≤j ＜k ＜i。

(d)fipq， 表示邏輯門xi的 輸入布爾賦值為(p,q)時的輸出布爾值。

為了降低變量個數(shù)，其中fipq中的fi00不會出現(xiàn)，因為常規(guī)布爾鏈中fi(0,0)=0。

(2) 約束。約束包含基本約束和擴展約束，其中基本約束確保能夠得到正確結(jié)果，而擴展約束通過邏輯網(wǎng)絡(luò)的特性加入了對稱性破拆(symmetry breaking)規(guī)則以減少搜索空間[2]，受篇幅限制，本文僅介紹基本約束。

基本約束中，最核心的是確保布爾鏈中的邏輯門完成正確的邏輯運算，該約束又稱為主約束子句(main clauses)。對于0≤a,b,c ≤1， 且1≤j ＜k ＜i，主子句約束定義為該約束可翻譯為，若邏輯門xi的 輸入分別是xj和xk，且xi,xj和xk在 真值表第t位的值分別為a,b和c，那么邏輯xi一定執(zhí)行的是邏輯運算b?ic=a。此處a,b和c，可控制變量的極性。

此外，若邏輯門xi是輸出，那么xi的真值表一定是等于其中待綜合的布爾函數(shù)，因此添加約束

一共有4個ghi變量，其中有2個賦值為1，表示函數(shù)輸入對應(yīng)的邏輯門，可知g14=1,g15=0,g24=0,g25=1。一共存在9個選擇變量，賦值分別為

4 基于SAT的精確綜合研究進展

精確綜合中如何高效進行SAT編碼以便更快求解是關(guān)鍵，精確綜合可以在線(online)或者離線(offline)的形式應(yīng)用到大規(guī)模集成電路綜合中。既可應(yīng)用到邏輯綜合中的邏輯網(wǎng)絡(luò)重構(gòu)、布爾函數(shù)等價分類等場景中，也可面向后摩爾時代新興計算范式中的新型邏輯原語、設(shè)計約束開展綜合優(yōu)化。本節(jié)重點介紹精確綜合當(dāng)前的研究進展。

4.1 SAT編碼

現(xiàn)有SAT編碼僅定義了基本約束，SAT求解器在進行狀態(tài)空間搜索時，需要同時完成兩個任務(wù)：搜索邏輯網(wǎng)絡(luò)的結(jié)構(gòu)和搜索每個節(jié)點的邏輯操作符，因此隨著邏輯函數(shù)所需的計算步驟(節(jié)點數(shù))增多，SAT求解器返回解的時間相對較長。若邏輯網(wǎng)絡(luò)結(jié)構(gòu)已知則使SAT編碼問題變得容易，因此通過添加一種基于DAG拓撲族的約束，對邏輯網(wǎng)絡(luò)的結(jié)構(gòu)和其節(jié)點的功能進行編碼，可以極大程度上限制SAT求解器的搜索空間，實現(xiàn)更快找到最優(yōu)替換網(wǎng)絡(luò)。

Haaswijk等人[9]使用基于DAG拓撲結(jié)構(gòu)枚舉的精確綜合算法限制了SAT求解器的搜索空間。由于拓撲結(jié)構(gòu)的數(shù)量隨著邏輯門數(shù)量的增加而快速增長，作者由此提出一種全新的拓撲結(jié)構(gòu)-布爾圍欄(Boolean fence)，如圖3所示，對于擁有4個節(jié)點的邏輯網(wǎng)絡(luò)對應(yīng)的DAG族進行分類，每個圍欄對應(yīng)于一個總節(jié)點分布相同的DAG族。通過枚舉和使用該DAG族來約束基于SAT的精確綜合編碼，加速了基于精確綜合的各種邏輯優(yōu)化算法。文獻[3]在此基礎(chǔ)上，重新審視基于SAT的精確綜合的編碼問題，收集拓撲族中的結(jié)構(gòu)集，提出了3種優(yōu)化來加速編碼并減少運行時間。分別為：量化CNF編碼方案之間的差異及其對運行時間的影響；證明對稱破缺約束的積極影響；使用多線程SAT求解器對拓撲信息進行計算。結(jié)果表明，使用DAG拓撲族可以有效地減少精確綜合運行時間和提高精確綜合的應(yīng)用范圍，同時并行化精確綜合會大幅減少運行時間，這些改進對使用精確綜合的各種邏輯優(yōu)化算法有直接影響。

圖3 圍欄結(jié)構(gòu)

現(xiàn)有的SAT編碼較多采用的邏輯門集合L是2輸入邏輯門，布爾函數(shù)的空間十分大，其枚舉或者計算可能難以處理。因此，通過引入更多輸入的多數(shù)邏輯門數(shù)據(jù)結(jié)構(gòu)作為網(wǎng)絡(luò)的邏輯表示，在精確綜合中使用這些原語會減少運行時間，使最佳布爾鏈的邏輯重寫性能得到大幅提升。

Soeken等人[7]使用MIG作為基礎(chǔ)邏輯表示，減少了SAT的求解時間。MIG為同構(gòu)邏輯表示并且邏輯表達能力強，表達形式如圖4(a)所示。由于MIG規(guī)則的數(shù)據(jù)結(jié)構(gòu)，可以丟棄輸出極性變量并引入對稱破壞規(guī)則。使用該算法，能夠改進基于查找表(LookUp Table, LUT)的工藝映射后的面積和延遲。在此基礎(chǔ)上，Haaswijk等人[10]將MIG擴展到功能縮減的MIG (Functionally Reduced MIGs, FRMIG)，改進了MIG邏輯優(yōu)化和基于LUT的映射。文章引入了基于k-LUT映射和精確k-LUT分解的通用MIG優(yōu)化方法，可用于深度和面積優(yōu)化。文獻[11]引入一種更緊湊的邏輯表示異或多數(shù)邏輯圖(XOR-Majority Graphs, XMG)，可以實現(xiàn)更小的邏輯網(wǎng)絡(luò)，從而在面積優(yōu)化中擴大使用精確綜合的范圍。具體方法是改進了子網(wǎng)絡(luò)選擇策略，避免了枚舉，允許算法擴展到更大的子網(wǎng)絡(luò)，從而消除了預(yù)計算和存儲所有精確解的需要。Chu等人[12]通過引入M55輸入多數(shù)邏輯門 (majority-of-five)算子計算操作數(shù)最少的布爾函數(shù)，降低了SAT編碼的難度，從而加快SAT求解速度。作者利用5輸入多數(shù)算子的對稱性，以符號編碼的方法來表示節(jié)點的功能，以此減少變量的數(shù)量。此外，作者引入5輸入多數(shù)反相器圖(M5-Inverter Graphs, M5IG)進行操作，這是MIG的擴展，如圖4(b)所示，其中“ 〈〉 ”為多數(shù)邏輯門，在圖4(a)中為M3，在圖4(b)中為M5。

圖4 全加器邏輯網(wǎng)絡(luò)的不同多數(shù)邏輯表達

最后，Marakkalage等人[13]使用基于SAT的精確綜合分析在不同輸入邏輯門中，用于同構(gòu)邏輯表示的最優(yōu)邏輯原語。通過對5輸入和6輸入布爾函數(shù)NPN等價類進行結(jié)果分析，證明3輸入邏輯門在可表達性方面是最強大的。因此在基于SAT的精確綜合中，我們更希望邏輯算子為3輸入多數(shù)邏輯門。

4.2 邏輯函數(shù)等價分類及等價匹配

邏輯函數(shù)等價分類的目標(biāo)是按照分類規(guī)則找到互相等價的一組布爾函數(shù)，使用一個具有代表性的函數(shù)來處理其他布爾函數(shù)。根據(jù)使用變換的不同，邏輯函數(shù)等價分類分為多種，研究最多的是否定置換否定(Negation-Permutation-Negation, NPN)等價分類，其中N-P-N分別代表對輸入的補操作、對輸入的置換操作和對輸出的補操作。布爾函數(shù)等價匹配用來判定一個布爾函數(shù)與另一個布爾函數(shù)在功能上是否是等價的。NPN等價匹配是在給定的準(zhǔn)則下確定兩個邏輯函數(shù)是否屬于同一個 NPN 類，用于將函數(shù)與已知的函數(shù)庫進行匹配。在邏輯綜合中，隨著邏輯函數(shù)規(guī)模的不斷擴大，對NPN等價匹配的可伸縮性和靈活性要求變高，在眾多匹配方法中，基于SAT的匹配為綜合問題編碼為SAT公式提供了足夠的自由度，具有較高的可伸縮性和靈活性。因此，將基于SAT的精確綜合運用到NPN等價分類問題和快速NPN等價匹配算法中，在給定分類規(guī)則下找到最優(yōu)布爾函數(shù)，構(gòu)建更好的分類和更快的匹配等價布爾函數(shù)。

Haaswijk等人[1,14]提出了一種以3輸入運算符的組合復(fù)雜性為基礎(chǔ)，對所有4和5輸入函數(shù)進行分類的方法，同時使用基于SAT的精確綜合，取消枚舉所有布爾鏈的算法。該方法不僅可以用于計算NPN類和函數(shù)的數(shù)量，還可以用作精確綜合算法的基礎(chǔ)，基于將函數(shù)映射到其NPN類和NPN類到最優(yōu)布爾鏈的兩層預(yù)計算索引，如圖5(a)所示。文獻[15]在此基礎(chǔ)上，設(shè)計了類層次結(jié)構(gòu)以更快速進行NPN分類，如圖5(b)所示。在現(xiàn)有的算法中，所有的類都屬于一個級別，并且函數(shù)直接與這些最終的NPN類匹配，而具有類的層次結(jié)構(gòu)允許將函數(shù)匹配到第1級(L1)的中間類，這些中間類被進一步匹配到來自第2級(L2)的最終NPN類。該算法使用精確綜合分別通過計算真值表和輔因子中1的數(shù)量來確定輸出的極性和每個輸入的極性。如果某些輸入具有相同數(shù)量的1，則形成一個綁定組，并且它們的位置是不明確的。因此，在每個綁定組內(nèi)使用SAT計算一系列否定和排列，從而最小化函數(shù)真值表中的值，以分類具有相同數(shù)量1的輸入。

圖5 NPN結(jié)構(gòu)

Huang等人[16]以真值表為基礎(chǔ)，實現(xiàn)了完全指定布爾函數(shù)的基于NPN分類的快速布爾匹配算法。作者以真值表表示的6～16個輸入布爾函數(shù)的精確NPN規(guī)范形式為基礎(chǔ)，同時檢測對稱變量以增加算法的效率，并適度減少了內(nèi)存使用量。由于使用了真值表，變量數(shù)量呈指數(shù)增長，該算法計算更多輸入的函數(shù)會降低運行時間。對于更多輸入的函數(shù)，Zhou等人[17]使用了分層方法消除了重復(fù)計算，升級了變量對稱性減少了要枚舉的變換，準(zhǔn)確地對多達16個輸入的任何實用布爾函數(shù)進行分類。該快速NPN分類算法設(shè)計了移位輔因子簽名(shiftedcofactor signatures)，將相位枚舉和置換枚舉分開，并以成本感知規(guī)范形式最小化排列枚舉成本。精確綜合算法的輸入大小限制是由真值表表示引起的，而該方法可以使用BDD來實現(xiàn)，對于實際應(yīng)用中出現(xiàn)的任何輸入多達16個的布爾函數(shù)，該算法使精確分類問題首次可以得到有效解決。

4.3 布爾函數(shù)邏輯重構(gòu)

在邏輯優(yōu)化中，邏輯重寫/重構(gòu)(rewriting)通過對未優(yōu)化邏輯網(wǎng)絡(luò)進行模板模式匹配，用等效的最優(yōu)邏輯網(wǎng)絡(luò)進行替換，以達到優(yōu)化節(jié)點數(shù)或邏輯深度的目的。邏輯重寫一般通過切割枚舉(cut enumeration)算法將給定邏輯網(wǎng)絡(luò)劃分為更小的子網(wǎng)絡(luò)，對于任何子網(wǎng)絡(luò)，在邏輯功能一致的前提下，在其替代邏輯網(wǎng)絡(luò)中選擇一個最優(yōu)的邏輯網(wǎng)絡(luò)進行替換。由于SAT求解器在子問題中進行的決策更少，故求解子問題比求解原問題要快得多。因此，基于SAT的精確綜合常用于邏輯重寫的相關(guān)應(yīng)用中，通過降低SAT求解器的計算復(fù)雜度，實現(xiàn)更快找到最優(yōu)替換網(wǎng)絡(luò)。

Soeken等人[18]設(shè)計了一種名為“忙人綜合”(Busy Man's Synthesis, BMS)的高效深度降低邏輯重寫算法，根據(jù)輸入到達時間和最大深度給出延遲約束，使用SAT公式以在延遲約束下找到最小面積的網(wǎng)絡(luò)。該算法在工藝映射器上實現(xiàn)，其運行時間與切割的數(shù)量成正比，因此適用于大型網(wǎng)絡(luò)。結(jié)果表明，可以有效解決6輸入函數(shù)問題。文獻[19]通過擴展SAT公式，除了針對布爾邏輯網(wǎng)絡(luò)的大小或深度等傳統(tǒng)成本指標(biāo)進行優(yōu)化外，還考慮了需要同時考慮的許多復(fù)雜約束的優(yōu)化應(yīng)用。文章首先通過比較用于精確綜合的不同SAT編碼，考慮延遲約束，找到針對大小或深度的最佳優(yōu)化。其次考慮了復(fù)雜約束問題的精確綜合，并解決了由于不同原語引起的約束和由于必須執(zhí)行綜合的邏輯表示的限制。

上述精確綜合方法不能高效地為具有大于10個變量的函數(shù)找到緊湊的邏輯網(wǎng)絡(luò)，Riener等人[20]改進了精確綜合的可擴展性，提出了一種以k-LUT作為布爾邏輯網(wǎng)絡(luò)節(jié)點的重寫算法，適用性更加廣泛。作者使用支持布爾無關(guān)項(don't-care)的基于SAT的精確綜合引擎來即時計算替換項，并將所有可能的替換候選存儲在沖突圖中，從中計算出可兼容替換網(wǎng)絡(luò)的最大子集。在此基礎(chǔ)上，Riener等人[21]設(shè)計了一個通用的再綜合(resynthesis)框架，用于優(yōu)化用多級邏輯表示、切割計算算法和再綜合算法參數(shù)化的布爾邏輯網(wǎng)絡(luò)。該框架基于精確DAG感知重寫引擎，以即插即用的方式實現(xiàn)強大的優(yōu)化算法。使用不同的再綜合算法，包括遞歸的自上而下不相交支持分解、精確綜合和數(shù)據(jù)庫查找表的算法，可以應(yīng)用于不同的多級邏輯表示，例如AIG, MIG以及LUT網(wǎng)絡(luò)等，大大增加了算法的使用場景。

4.4 面向新興計算范式的精確綜合

新興計算范式采用新型邏輯原語和計算策略，如采用蘊涵、多數(shù)邏輯門、閾值門(threshold logic gate)等，近似計算則放寬了對邏輯函數(shù)的精度要求，加入了一個新的維度優(yōu)化PPA。因此，面向新興計算范式的綜合優(yōu)化面臨更多的優(yōu)化約束，且缺乏可參考的設(shè)計。而精確綜合可以有效對約束進行SAT編碼并求解。

近年來，可逆邏輯電路的綜合逐漸受到重視，同時還有其他基于函數(shù)轉(zhuǎn)換或更高級別的函數(shù)表示的方法，如異或乘積和(Exclusive-or Sum-Of-Products, ESOP)，它們能夠處理更大的電路，雖然其特點保證無需其他最優(yōu)性或接近最優(yōu)性的約束，但找到具有最少乘積項的ESOP形式是精確綜合的目標(biāo)。基于SAT的精確綜合常被運用在可逆電路或高級函數(shù)表示的綜合方法中。對于實現(xiàn)所需功能的電路，精確綜合算法確定給定功能的最小電路實現(xiàn)，即分別具有最少門數(shù)或成本的電路。

Gro?e等人[22]在具有正控制線的Toffoli門電路中，分析SAT以及Toffoli門的特點，設(shè)計了適用于Toffoli門的SAT編碼。設(shè)計的迭代算法將Toffoli網(wǎng)絡(luò)綜合問題表述為一系列決策問題，可以找到更小的給定函數(shù)，該選擇編碼方式對于生成最優(yōu)網(wǎng)絡(luò)至關(guān)重要。Wille等人[23]則在帶有負控制線的Toffoli門中，實現(xiàn)了SAT編碼?？紤]負控制線會導(dǎo)致電路比目前最優(yōu)邏輯門數(shù)量的實現(xiàn)更小，所組成的可逆電路的精確綜合效率更高。Kole等人[24]在此基礎(chǔ)上，實現(xiàn)了3元可逆邏輯的基于SAT的精確綜合。作者將表示可逆3元真值表的置換作為輸入，將由實現(xiàn)置換的廣義3元Toffoli門組成的可逆電路作為輸出。該方法提供了一個基準(zhǔn)，可以與其他非精確綜合的性能進行比較。

Riener等人[25]通過將ESOP綜合問題編碼為SAT問題，提出一種使用SAT計算ESOP形式的精確綜合方法，為給定的布爾函數(shù)找到1個或多個ESOP形式。類似于自底向上的基于SAT的精確綜合，作者從可能不完全指定的布爾函數(shù)形式的規(guī)范開始，迭代地構(gòu)造一個布爾約束滿足問題，當(dāng)且僅當(dāng)具有實現(xiàn)規(guī)范的k(最初k=1)乘積項的ESOP形式存在時，該問題是可滿足的，并返回具有k個乘積項的ESOP形式。這種基于SAT的精確綜合方法不依賴應(yīng)用于一對乘積項的立方變換，而是能夠優(yōu)化乘積項的小子集，有望成為新一代啟發(fā)式ESOP優(yōu)化方法的支柱。

隨機計算(Stochastic Computing, SC)使用轉(zhuǎn)換為隨機比特流的二進制數(shù)實現(xiàn)計算復(fù)雜的算術(shù)，SC的容錯特性使其被應(yīng)用在大量應(yīng)用中。然而隨機電路綜合允許比經(jīng)典邏輯綜合更大的解決方案空間，以往的啟發(fā)式方法只探索有限的解空間子集，無法保證結(jié)果的最優(yōu)性，因此基于精確綜合的方法被大量運用在SC中。

Wang等人[26]提出了一種基于輸入誤差邊界進行搜索的方法來尋找目標(biāo)函數(shù)的最佳逼近多項式，保證了最佳逼近多項式的最優(yōu)性。為了優(yōu)化電路的大小，作者在精確綜合過程中考慮邏輯門面積的方法，并設(shè)計了基于SAT的精確綜合方法，可以直接綜合面積最優(yōu)的SC電路，無需工藝映射，同時提出了部分賦值(Partial Of Assignment, POA) 和多粒度搜索(Multi Granularity Search, MGS)來減少SAT求解器的搜索空間。He等人[27]以MIG作為基本邏輯表示，使用基于SAT的精確綜合來綜合最佳SC電路。作者使用立方體賦值(cube assignment)分解問題向量，以解決可擴展性問題，加速精確綜合。同時，為了探索任意大小的通用電路，作者設(shè)計了一種基于精確綜合和啟發(fā)式的混合算法，其中精確綜合被用作決策者來減少解樹中的分支數(shù)量，從而得到更小的面積延遲積。

作為一種內(nèi)存計算的方法，憶阻電路允許數(shù)據(jù)存儲和邏輯運算。Chen等人[28]提出了一種精確綜合方法來推導(dǎo)蘊涵(IMPLication, IMPLY)邏輯網(wǎng)絡(luò)，對所有3輸入布爾函數(shù)進行綜合，無需中間步驟即可直接獲得最優(yōu)的 IMPLY 邏輯網(wǎng)絡(luò)，較基于AIG的綜合算法比有優(yōu)化。

5 展望

由于精確綜合的高計算復(fù)雜度，以上所提出的精確綜合算法對小函數(shù)優(yōu)化具有較高的效率，但它不適用于超大規(guī)模函數(shù)，直接對大規(guī)模邏輯網(wǎng)絡(luò)進行精確綜合尋優(yōu)面臨困難。SAT編碼的優(yōu)勢在于它可以靈活地處理不同的成本函數(shù)，并且可以擴展到不同的場景。因此，將基于SAT 的精確綜合算法應(yīng)用于大型函數(shù)的小型子網(wǎng)絡(luò)，可以保證大規(guī)模網(wǎng)絡(luò)的局部最優(yōu)性。本節(jié)簡要闡述了目前精確綜合所面臨的困境和挑戰(zhàn)，并嘗試對未來可能對精確綜合產(chǎn)生重大影響的新技術(shù)進行了討論，同時對未來的發(fā)展趨勢進行預(yù)測。

5.1 SAT編碼

首先，選擇合適的SAT編碼方法和SAT求解器的不同啟發(fā)式算法會在一定程度上優(yōu)化精確綜合運行時間。文獻[1]表明，選擇編碼和對稱性破拆的正確組合會極大地影響綜合運行的時間，并且選擇合適的SAT求解器啟發(fā)式算法同樣會加速精確綜合的運行時間。因此一個研究方向是開發(fā)專門解決精確綜合問題的特定領(lǐng)域SAT求解器，文獻[29]考慮到精確解可以幫助精確綜合求解加速，設(shè)計了一種基于半張量積的SAT求解器，通過矩陣數(shù)理計算替換傳統(tǒng)布爾邏輯運算的新型求解方法，得到SAT問題的全部精確解，可以用于篩選精確綜合的最優(yōu)解，提高求解的質(zhì)量和速度。文獻[30]中，一種基于電路信息的SAT求解器已經(jīng)成功應(yīng)用于邏輯綜合算法。由于該求解器可以事先知道問題邏輯網(wǎng)絡(luò)的結(jié)構(gòu)，其具有更快的約束傳播和可變的啟發(fā)式方法。

5.2 DAG拓撲結(jié)構(gòu)

其次，選擇合適的DAG拓撲結(jié)構(gòu)可以顯著減少精確綜合運行時間。文獻[3]中，一個未解決的問題是需要搜索或生成“好”的DAG拓撲。例如，某些DAG可以表達更多信息或某些拓撲比其他拓撲可以表示更多的功能，因此能否找到一些特征來表征更具表達性的特定DAG拓撲。未來的工作中可以根據(jù)不同的策略找到枚舉拓撲結(jié)構(gòu)，以實現(xiàn)進一步的加速，或構(gòu)建條件概率分布，在給定函數(shù)下，可以使用哪些類型的拓撲來表示該函數(shù)。此外，只需要檢查包含潛在有效拓撲的空間部分，利用DAG拓撲即等于劃分綜合搜索空間。另一個研究方向是使用基于圖的拓撲作為基于SAT的精確綜合算法的基礎(chǔ)，作為其并行性的來源。

5.3 人工智能

最后，利用人工智能(Artificial Intelligence,AI)技術(shù)優(yōu)化EDA中的算法受到廣泛關(guān)注[31]。傳統(tǒng)啟發(fā)式算法通常需要對每個待求解問題進行初始化，在面對邏輯綜合優(yōu)化問題時需要大量的時間和資源，缺乏知識積累。相反，機器學(xué)習(xí)可以用于自動學(xué)習(xí)新的邏輯綜合算法或改進算法本身，避免重復(fù)的復(fù)雜分析。因此，基于AI的邏輯綜合方法是解決這一問題的有效途徑之一。

許多邏輯綜合優(yōu)化問題可以歸結(jié)為組合優(yōu)化問題?；贏I的方法，一方面可以利用AI推理確定綜合流(synthesis flow)，例如，邏輯綜合引擎反復(fù)對子電路進行平衡(balance)、重寫(rewrite)、重構(gòu)(refactor)和重替換(re-substitution)等變換，以提高結(jié)果的質(zhì)量。另一方面對邏輯網(wǎng)絡(luò)進行自動劃分，智能推斷所采用的綜合策略。在精確綜合方面，AI可以對如何劃分小規(guī)模電路進行學(xué)習(xí)，提高子電路的質(zhì)量；同樣也可在給定不同邏輯原語集合的情況下，對劃分后的子電路進行精確綜合，并有效評估綜合的效果，確定是否為最優(yōu)網(wǎng)絡(luò)。

6 結(jié)束語

精確綜合是一種通用的邏輯綜合技術(shù)，可應(yīng)用于邏輯優(yōu)化、工藝映射、新興技術(shù)的綜合等。對于傳統(tǒng)精確綜合，存在運行時間無法預(yù)測，不足以有效地為具有大于6個變量的函數(shù)找到面積或深度最優(yōu)的邏輯網(wǎng)絡(luò)等問題。與傳統(tǒng)手段相比，近年來，隨著SAT約束求解能力的進步，結(jié)合SAT約束求解的精確綜合確定為進一步發(fā)展的方向，其性能也得到了大規(guī)模提升。同時，基于SAT的精確綜合可以集成任意約束，實現(xiàn)在任意條件下的高效精確綜合，為新興納米電路物理條件約束下的綜合提供全新思路。