背景介紹

Combinational ATPG是一個Branch and Bound的演算法，它的本質是在組合電路（Combinational Circuit）內找到適合的輸入向量（Input Vector）工具。所有輸入訊號的可能組合形成輸入空間（Input Space）。這個輸入空間的大小主要和組合電路內Primary Inputs的數量有關，它會形成一個二元樹（Binary Tree），每個節點（Node）有兩個分支（Branch），節點上的符號代表輸入訊號的代號，假定左邊的分支代表該Node輸入值為0，右邊的分支代表該Node輸入值為1。ATPG用DFS（Depth First Search）可以在輸入空間內找到一條路徑（Tour），當所有輸入訊號（Input）的值依照這條路徑輸入進去電路設計的時候，能夠滿足某個我們想觀察的性質（Property）。

由於輸入空間這個二元樹的節點數量太大，需要一個更有效率的資料結構才能夠在有限的記憶體空間內表示它；另外一方面人們也致力於發展如何縮小這個輸入空間以及更聰明的尋訪該輸入空間的方法。

隨著BDD（Binary Decision Diagram）這類資料結構的提出，人們也應用它來解決ATPG中輸入空間過大的問題。其中對於ROBDD（Reduced Order Binary Decision Diagram）除了有著一些時間複雜度不高的運算之外，它有個很好的特點，就是處理的問題如果被處理成ROBDD的格式後，最後簡化成相同的ROBDD表示這兩個問題是一致的（Canonical），換句話說兩個功能相同的電路個別表示成ROBDD的格式時該ROBDD的表示法是唯一的[3]。

《圖一　由Binary Tree轉化成BDD》

在ATPG中使用BDD技術最主要是運用有效的資料結構來在有限的記憶體空間內表示它。運用BDD為ATPG Engine的技術在中小型的電路結構裡，它的能力大約可以處理上百個變數的輸入空間。但是現今的電路設計已經超過了這個範疇，尤其是把循序電路（Sequential Circuit）考慮進去性質為真否的證明時，BDD往往會面臨Memory Explosion的窘境。

組合電路的Solver

將SAT（Satisfiability）problem應用到驗證上是90年代有著長足進步的ATPG技術，這方面研究的進步讓我們在一個組合電路之中，可以把電路轉化成SAT的問題，研究的對象從原來的邏輯電路的推導，簡化成在Boolean Domain的Conjunctive Normal Form（CNF）做布林運算（Boolean Operation）[1]。

《圖二　基本閘轉換成SAT Equations[1]》

這種簡化有著什麼樣的影響？原來使用ATPG要處理的資料結構變簡單了，不需要像從前一樣從輸入訊號端把訊號一層層傳送（Propagate）到輸出訊號（Output）端。另外把原來的問題轉換成CNF後，有一些很有趣的性質被注意到也藉此加速了ATPG的運作。

Implication/Unit Clause Rule──SAT問題是一個以上的Clauses組成CNF，亦即POS（Product of Sum），然後求ㄧ組變數的Assignment讓整個POS的值為TRUE。當任何一個Clause裡面的變數都被分配成FALSE，整個POS的值將會是FALSE。因此當一個Clause裡面只剩一個變數沒有被分配到值的時候且其他同一個Clause裡的變數值都為FALSE，該變數舊的值就馬上被決定為TRUE，換句話說即不用尋訪該變數為FALSE的分支子樹。

《圖三　Implication/ Unit Clause Rule[1]》

Conflict Learning──SAT在分配變數的過程中即使運用了Implication依然會遇到分配的變數而讓某個Clause產生在該Clause內的所有變數都為FALSE的狀況，該情形為產生一個Conflict。直覺的解決方法就是Backtrack回到之前可以分配別的值的變數走另外一條分支。但是其實產生Conflict的時候SAT可以找到一些資訊，而且這些資訊就藏在剛剛那個產生Conflict Clause的變數分配過程之中，我們用下面幾張圖表示學習（Learning）的過程。

《圖四　學習的過程[1]》

Conflict Learning最重要的特點就是，經它學習加入SAT的Conflict Clause只要證明的性質不變，即使經過Backtrack或變數的分配順序改變這個Conflict Clause依然可以一直被重複使用。

Variable Ordering──一個好的變數分配順序也會決定整個解SAT問題的效率，因為它直接關係到尋訪時的路徑。比較(圖五)中兩棵樹的分支情形，發現同樣學習到的資訊但是不同的變數分配順序對於整顆輸入空間樹刪去（Prune）其分支不用尋訪的情形也會不同。

《圖五　Different Variable Ordering對Search Space的影響[1]》

SAT也有它的一些問題：

第一點即為加入Backtrack的機制，在ATPG找到一組解的時候繼續尋訪其他的分支；第二點則是仍待研究的問題；至於第三點則是要待有Preimage/Image的觀念才能繼續解答。

循序電路的Solver

從數學的角度看一個函數y=f(x)，一個合理的x的值可經由該函數對應到一個合理的y的值。所有合理的x值的集合稱作Preimage，而所有合理的y值的集合即為Image。

剛剛的觀點對應到組合電路，所有合理的輸入訊號形成的集合稱作Preimage，所有合理的輸出訊號形成的集合稱做為該電路的Image。但現今使用的晶片大多是被設計成循序電路的樣子，下面以一個簡單的概念圖表達循序電路的組成以及它和組合電路之間的關係，如(圖六)所示[2]。

《圖六　圖左為SI、SO、PI、PO、Register；圖右為展開的概念 》

所以循序電路在多個clock cycles內的行為可以由展開（Unfold）組合電路來描述，原來在組合電路裡面輸入訊號只有Primary Input，輸出訊號只有Primary Output。循序電路裡面輸入訊號除Primary Input之外還包括上ㄧ個cycle結束時暫存器（Register）的狀態，即圖六的Pseudo Input；循序電路裡面輸出訊號除了Primary Output之外也包含這一個cycle裡面將要被存入站存器的值，即圖六的Pseudo Output。因此在循序電路中Preimage可以看作是在每個clock cycle裡面合理的輸入訊號形成的集合，而Image是每個clock cycle裡面合理的輸入訊號形成的集合。

Preimage/Image的重要性在於提供循序電路中驗證電路的線索，通常設計者運用模擬（Simulation）電路運作的方式來進行除錯與驗證的工作，但在電路設計日趨繁瑣的今天要完整的運用模擬的方法檢查所有可能的輸入訊號組合已經不是合理時間內可以完成的。此外，就Assertion來說，如何在一個循序電路內檢查一個性質是否在任何時間點恆真，像這類問題光靠模擬已經不能解答。

《圖七 循序電路檢查Assertion是否成立示意圖[4]》

在(圖七)表達在一個循序電路中檢查一個Assertion是否成立時通常採取的作法。假定這個Assertion希望驗證電路裡面正常運作情況下a>b該性質永遠成立，這時候會在原來的邏輯電路加入一個比較器並且將該比較器的輸出(c)看成是一個Primary Output。如果能夠證明在電路正常運作的情況下形成的Preimage會讓c的輸出值一直為真（TRUE），這個Assertion就成立了[4]。

希望應用ATPG證明上面的命題，以ATPG的角度來講，ATPG是一個搜尋合理解的過程，沒有辦法正面回答在所有輸入情況下c的輸出值皆為1，但是可以嘗試著去找出一個輸入訊號的組合讓c的輸出值為0。如果找到了這種輸入訊號的組合，就可以駁斥這個命題；反之，如果找不到這種輸入訊號的組合，也可以間接證明上面的命題[6]。

由於現今發展出來的晶片都屬於有限狀態機（Finite State Machine）， 所以Preimage的大小有限，雖然如此就算只考慮一個cycle內電路輸入訊號的所有可能情況，即為其輸入空間的大小，假設電路內有50個暫存器與50個Primary Inputs，會得到輸入空間的大小為2100。再把如果產生出違反這個性質的結果是經過多個cycle的轉換（Transition）考慮進去，這個輸入空間又會更大，可以預期如果使用原來用在組合電路的ATPG應用在這問題上，勢必要花更多時間和更多記憶體空間。但最重要的是不可能靠無限的展開電路把循序電路的問題轉化成組合電路再去給ATPG解。

要解決這個問題，從數學的角度來看如何求x=f(x)中x的所有解集合。首先是從初始的x值開始帶入f(x)，來求出x的一個解集合，然後在將此解集合帶入f(x)，求出下一個解集合，這樣的步驟反覆代入幾次之後。最後，會達到一個解集合X，使得X=f(X)，亦即是所謂的fixed point，而這個X就是x=f(x)的所有解集合。

從解循序電路的問題來看，上述的方法就像是從起始的狀態（Initial States）經過一個clock cycle來求出下一個時態的狀態集合。而將這些狀態帶入電路，則可以求出下一個時態所有狀態的集合。這樣子反覆代入之後，最後，可以求出一個狀態的fixed point。亦即是由起始狀態開始電路可以到達的所有狀態的集合（Set of Reachable States）。

想驗證的assertion命題會形成一個Image Space，利用求出其Preimage的方法會發現如果Preimage到達fixed point時有和Initial State的集合有交集，就表示這個assertion的性質不成立，反之如果沒有交集則成立。也可以試著從Initial State出發如果找到Initial State可以到達的Image的fixed point時，發現該Image有和assertion命題形成的集合有交集，就表示這個assertion的性質不成立，反之如果沒有交集則成立[6]。

《圖八　Preimage和Property形成的Image沒有交集的情形 》

傳統上人們是使用BDD來尋找Preimage/Image的fixed point，然而使用BDD會有Memory Explosion的問題。因此人們開始使用SAT-based的ATPG演算法並修改讓它能夠在找到一個解之後Backtrack回來繼續找下一個解，直到它找到所有的解為止。

舉例來說，下面提出的方法裡面，作者修改了原來PODEM的ATPG演算法讓它能夠應用到循序電路上，此外，這個方法提出一個新概念──Success-driven Learning[5]幫助ATPG刪減掉更多輸入空間的分支。為了避免表示Preimage/Image時花費太多記憶體，使用BDD來儲存它們。

Success-driven Learning和Conflict Learning有什麼不同呢？簡單來說，Conflict Learning是從Conflict產生的地方學到有用的資訊，而Success-driven Learning是從ATPG結果成功的地方分析出有用的資訊。

Conflict Learning：

Success-driven Learning：

結論

總而言之，近年來ATPG與SAT在解combinational與sequential上，提出了許多新的演算法（algorithms），人們進一步尋求簡化ATPG問題的方法。Abstraction and Refinement[6]是最新的方向之一。運用原有對Preimage/Image的了解，希望能夠把原來的命題先抽象化（Abstraction）成一個比較小的SAT問題，看看該性質在比較小的SAT問題裡面有沒有解，如果有解表示原來的命題也會有解，如果沒有解，再去確定是不是在原來的命題範圍裏面沒有解。如果沒有解的結論是FALSE，就進行重新修正（Refinement），希望得到一個更接近原來命題的SAT問題，反覆直到找到解或證明真的沒有解為止。

希望ATPG的進步不只在未來能夠找到在循序電路內有更有效率的驗證方法，另外也希望能夠利用更多關於電路上的資訊，提升ATPG Engine朝向Word Level ATPG做更高階的應用。（作者為台大電子工程學研究所/台大系統晶片中心研發教授?黃鐘揚；研究生林庭豪）

＜參考資料：

[1] Sharad Malik“The Quest for Efficient Boolean Satisfiability Solvers” http://www.princeton.edu/~sharad/

[2] 台灣大學電子所課程 VLSI Testing, 2004

[3] 台灣大學電子所課程 (超大型積體電路)電腦輔助設計系統概論

　 http://cc.ee.ntu.edu.tw/~ywchang/Courses/EDA/eda.html

[4] 台灣大學電子所課程 系統晶片驗證 (SoC Verification)

[5] Efficient preimage computation using a novel success-driven ATPG," Shuo Sheng and Michael S. Hsiao, in Proceedings of the IEEE Design Automation and Test in Europe Conference, March 2003, pp. 822-827.

[6] E. Clarke, O. Grumberg, S. Jha, Y. Lu and H. Veith, “Counterexample-Guided Abstraction Refinement.” In Proceedings of CAV, pp. 154-169, July 2000.＞

延 伸 閱 讀

當IC逐漸演化成內部電路錯綜複雜的SoC，以往單純的測試程序也跟著高難度了起來；為了提高這道SoC“健康檢查”程序的效率，在前段IC設計中採用可測試性設計（Design for Test；DFT）技術，成為市場接受度越來越高的解決方案。相關介紹請見「 DFT讓SoC“健康檢查”更有效率」一文。 近年來由於積體電路製造技術日新月異以及為了縮短電子產品上市時間，單晶片系統的設計技術扮演著舉足輕重的地位，其中嵌入式記憶體常用於單晶片系統，因此如何對一嵌入式記憶體作一有效的測試是一個值得重視的問題。 你可在「 半導體記憶體之測試研究」一文中得到進一步的介紹。 在產品日趨輕薄短小，功能日益複雜的前提下，朝高整合度的系統單晶片（System on Chip；SoC）發展之途，已成為未來半導體產業演進的終極目標。由於SoC的系統設計整合了多項不同功能的電路在相同的IC上，測試上也不同於以往將單功能的IC個別測試後，即可組成系統；取而代之的是高複雜度的SoC測試技術。在「SoC測試技術探索」一文為你做了相關的評析。

市場動態

Mentor Graphics宣佈其行業領先的自動測試向量生成工具（ATPG）、FastScan以及它的嵌入式確定性測試工具TestKompress新增加自動化處理功能——ATPG Expert。ATPG Expert功能部件能對設計進行自動分析，並智慧化地使用ATPG工具（Fastscan和Testkompress）所提供的命令處理測試向量生成中的所有複雜性，如RAM的Shadow logic和匯流排衝突問題。你可參考 「Mentor Graphics宣佈FastScan和TestKompress測試設計工具增強自動化處理功能，取得最佳的測試覆蓋成果」一文。 SynTest宣佈推出DFT-PRO 100和200系列入門級ATPG (Automatic Test Pattern Generation)套裝軟體，該套裝軟體包括用於複雜ASIC測試的基本DFT (Design-for-Test)工具，這些工具可對已插入掃描鏈的網表進行作業，其中包括具有以下用途的工具：測試DFT規則違反、自動測試向量生成(ATPG)和測試向量格式轉換以便和Advantest、Agilent、Credence及Teradyne等供應商的ATE相容。 你可在「SynTest發佈ATPG入門級套裝軟體可提高ASIC設計品質」一文中得到進一步的介紹。 以往的系統設計是將CPU，DSP，PLL，ADC，DAC或Memory等電路設計成IC後，再加以組合變成完整的系統，但現今的設計方式是將上述的電路直接設計在同一個IC上，或購買不同廠商的IP（intellectual property），直接加以整合，此方式稱為系統單晶片（SoC)設計方法。SoC方式降低設計和製造成本，但對於測試來說卻變得更為複雜，測試成本也越來越高，測試問題已不容忽視。在「SOC晶片設計與測試」一文為你做了相關的評析。