驗證（verification）是現代數字集成電路設計流程中不可或缺且至關重要的一環，其目的是保證設計功能按照既定的設計規約正確的實現。在一個完整的項目周期中，驗證所占用的時間可高達60%-70%。按驗證的具體目的，可以有很多種細分類別，而本文主要針對其中的“功能驗證“，即只專注于設計邏輯功能的實現，而暫不考慮綜合、布局布線后引入的電路延時與優化，從而導致的硬件與實際邏輯出現偏差的情況。

目前業界主流的驗證方法主要是以UVM（Universal Verification Methodology）為代表的驗證方法學，通常使用隨機約束的方式，在電路仿真中自動產生受控的隨機輸入，從而驅動驗證電路并完成驗證功能。隨著UVM的發展和廣泛使用，特別是其中SystemVerilog語言加入了面向對象、功能覆蓋、隨機約束等更加類似軟件開發的特性，使得驗證平臺間模塊重用的效率得到提升，編程結構化變好，代碼更加靈活。有關這些傳統的驗證方法的討論和思考會在下文中逐步給出。

然而需要注意到的是，這些基于電路仿真的驗證方法存在較多的根本性問題一直無法有效解決，如對極端情況的覆蓋、過長的仿真時間、調試難度較大等等。這些問題也將會在后文一一討論。在2018年初，幾乎全部主流的CPU廠商都被發現在其CPU產品中存在熔斷（Meltdown）和幽靈（Spectre）漏洞。這也在一個側面表明，當代集成電路驗證存在極高的復雜性，特別是對于大型設計而言。因此，業界一直在尋找其他更為有效的驗證方法學。下文將介紹的“形式化驗證“（Formal Verification）就是其中之一。

圖1：熔斷（Meltdown）和幽靈（Spectre）漏洞

什么是形式化驗證

和基于電路仿真的驗證方法不同，筆者認為形式化驗證的定義是：利用形式化方法，即基于嚴格的數學表述和模型，根據設計規約對設計功能進行屬性描述，并自動進行數學分析和證明。這看上去似乎非常玄妙，但實際上形式化驗證的過程可以粗略的由下圖描述：

圖2：形式化驗證簡要流程圖

它很像我們上學時做過的數學證明題，即給一個命題，用數學定理和方法證明該命題是否成立。若不成立則給出一則反例。在形式化驗證中，待測設計的某個功能和設計規約對應的描述就是命題的兩部分，命題為證明二者是否等價，若得證則表示在任意情況下命題成立，若不得證則表示命題不成立，且會給出一個反例。這個推理和證明的過程通常由EDA工具自動完成。目前，業界主流的形式化驗證EDA工具主要有Cadence的JasperGold，和Synposys的VC-Formal等。

需要注意的是，作為形式化驗證的使用者，我們并不需要了解形式化方法的具體數學原理，亦或是證明的具體過程。在多數情況下，在形式化驗證工具里的調試過程和傳統電路仿真工具十分類似。在下一章，我將詳細介紹形式化驗證相比傳統驗證方法的主要優勢。

形式化驗證的主要優點

與傳統的基于仿真的驗證方法相比，形式化驗證主要有以下三個方面的優點。

第一，形式化驗證能覆蓋完整的設計狀態空間。

與其他所有基于仿真的驗證方法相比，這一點是形式化方法最大的優勢所在。通常來講，一個數字電路的設計通常由若干個邏輯狀態空間（logic state space）組成，這其中可以包含以下幾類狀態：

電路復位后的初始化狀態， 也稱為復位狀態；

內部邏輯實現時的中間狀態；

各個輸入輸出的狀態。

比如，在一個FIFO設計中，它的“滿”、“空”指示就是輸出的狀態；在某一時刻，FIFO里內存的讀寫指針的位置就是中間狀態；而當復位完成后，指針位置以及當時“滿”、“空”指示的值就是復位狀態。

如果將這些狀態抽象提取出來，我們可以得到針對這個設計的完整的狀態空間，如下圖所示，其中每一個圓圈都代表電路中的一個可能的邏輯狀態。而驗證的最終目的，就是對完整的狀態空間進行覆蓋，并確定其滿足既定的設計要求。

在電路仿真中，每次仿真實際上就是在狀態空間里尋找一條從“復位狀態”到“輸出狀態”的路徑， 如下圖中標出的一條路徑。

圖3：一次仿真得到的狀態路徑

需要注意的是，在仿真中每條路徑的確定與仿真使用的輸入（也稱為激勵或測試向量）有著密切的關系。如果在每次仿真中使用不同的輸入，例如采用隨機約束的驗證方法，那么有可能找到更多的狀態路徑，如下圖所示。

圖4：多次仿真得到的狀態路徑

然而，對于某些大型設計，即便使用了多種不同的輸入，也有可能仍然找到相同或者部分重疊的路徑，這樣就導致某些狀態很難被覆蓋，即我們通常所說的“邊界情況”（corner cases）。對于邊界情況的處理，通常的做法是增加仿真次數，即嘗試更多不同的輸入組合；延長仿真時間；或者針對其創建新的“定向測試”等。然而不管使用何種方法，都會極大的增加完成驗證所需的時間，以及投入的各類成本。最根本的問題在于，即便使用了這些方法，也并不能保證邊界情況被100%覆蓋，這是由于仿真無法遍歷所有可能的輸入向量。換句話說，基于仿真的驗證只是檢驗了在使用某些測試向量時，系統不會出現漏洞，但無法保證當使用其他測試向量時，漏洞不會出現。上文提到的CPU “熔斷”和“幽靈”漏洞，也從另一個角度很好的印證了這一點：一方面，我相信英特爾（及其他廠商）在設計芯片時已經進行了充分驗證，但顯然還存在邊界情況。另一方面，即使芯片已上市并廣泛使用多年，這些漏洞直到最近才被發現，這在一定程度上表明通過改變測試向量來進行邊界情況的捕捉和覆蓋，效果不夠理想，往往更像是“大海撈針”。

形式化驗證和基于電路仿真的驗證方法的最根本不同在于，形式化驗證并不基于某些給定的輸入向量，而是通過數學方法分析、推導并證明某個邏輯功能在給出的邊界范圍內是否與設計規約完全吻合，若不吻合則會給出一個反例。在上面舉的例子中，形式化驗證可以從給定的復位狀態開始，用數學方法自動探索并覆蓋整個狀態空間，如下圖所示。從形式化的視角來看，這里所有的邏輯狀態并沒有本質的區別，因此即使是電路仿真很難發現的邊界情況，也能很容易的通過形式化的方法進行覆蓋。

圖5：形式化驗證對狀態空間的全覆蓋

通常而言，上述數學推理并證明的過程都被封裝在EDA工具里，并由工具自動完成。因此作為形式化驗證工具的使用者，我們并不需要深入理解這些工具的工作機制，以及其中復雜的數學理論。這進一步降低了形式化驗證的使用門檻，同時能讓設計和驗證工程師從更為整體的角度思考驗證策略，而非糾結于如何產生各類輸入向量才能達成某種設計中的狀態。

第二，形式化驗證能提供最小實例

形式化驗證的第二個主要優點在于能迅速提供一個最小實例，如下圖所示。這里“最小實例”指的是，達到一個目標狀態所需要的必要條件，包括各個輸入值、寄存器的狀態，以及達到目標狀態需要的最少周期數等。

圖6：形式化驗證可以提供到達目標狀態的最小實例

設想在一個復雜的狀態機設計中，需要驗證某個狀態能否實現，且需要考察達到該狀態時所需要的條件， 比如：如何給定輸入、內部狀體如何轉換、通過多久才能達到該狀態等等。如果使用電路仿真，會有以下幾個問題：

1. 由于不確定何種輸入向量才能達到目標狀態，首先需要進行一系列仿真才有可能達到該狀態。若目標狀態恰好是邊界狀態，找到它本身的難度就很大。

2. 即使通過多次仿真找到了滿足條件的輸入向量，這樣每次的仿真時間往往長達幾十分鐘到幾小時，對復現和多次調試的效率影響很大。

3. 無法確定是否還有其他條件能夠達到目標狀態。

和電路仿真不同，形式化驗證可以很快的給出達到目標狀態的最小實例，或者反之，得出結論證明該目標狀態永遠不會被達到。電路設計者和驗證者可以通過這個特性，利用形式化驗證對目標狀態進行快速調試，并通過給出的最小實例，更好的理解電路行為，及時發現其與設計規約的偏差。

第三，形式化驗證能提供“基于狀態”或“基于輸出”的分析和調試方法。

如上文所述，傳統的電路仿真都是基于輸入的方法，即給出輸入后才能觀察內部狀態以及電路輸出。然而，形式化驗證并不依賴任何輸入，因此可以做到“基于狀態”或者“基于輸出”，并以此進行設計分析和調試。

例如，在基于狀態的方法中，我們希望知道在一個設計中是否能夠通過某種方式達到某種狀態（如前文中所述），或者更進一步，希望將此狀態作為接下來分析和調試的起始狀態?？梢韵胂螅褂秒娐贩抡孢_成這樣的目標很難，因為需要先找到合適的輸入、經過漫長的仿真時間后才可能達到該狀態，而往往對于固定的輸入只會得到固定的輸出，如下圖所示。

相比之下，形式化驗證沒有這些限制，而是可以任意指定起始狀態，并可以由該狀態為起點，探索后續的所有可能的狀態空間，包括所有可能達到的輸出狀態，并給出對應的輸入最小實例。同理，甚至可以指定某個輸出狀態為目標狀態，由此反推達到該狀態需要滿足何種條件。

圖7：形式化驗證可以進行基于狀態或輸入的調試和驗證

形式化驗證的主要缺點

形式化驗證有著傳統基于仿真的驗證方法學無可比擬的優勢，看起來幾乎是完美的驗證方法學。可惜的是，形式化驗證有著非常顯著的缺點，其中最主要的就是所謂的“狀態爆炸”問題（state explosion）。顧名思義，這代表了在某個設計中，理論上存在的狀態可能非常多，超出了形式化驗證工具可以處理的范圍。例如，在一個簡單的n位計數器中，可能存在2^n個狀態，且狀態數量隨著計數器位數的增加呈指數級增長。同樣的狀態爆炸問題存在于存儲器、各類數學運算單元如乘法器等等。

可以看到，這個問題是由形式化驗證——具體而言是形式化驗證中最為常用的模型驗證（Model Checking）——的工作機制決定的，是形式化驗證的根本性問題，無法通過優化算法或者工具完全解決。但是值得欣慰的是，學術界和業界也在不斷探索用來緩解狀態爆炸問題的各種方法。在理論上，有學者提出了以下方法，如：

符號模型驗證（Symbolic Model Checking），即使用二元決策圖（Binary Decision Diagrams – BDD）而非獨立的狀態列表來表達狀態空間；

偏序約減（Partial Order Reduction），即檢查各個狀態和行為間的獨立性以減小整體的狀態空間；

基于反例的抽象優化（counterexample-guided abstraction refinement），即自適應的尋找合適的抽象層次，實現精度和運行時間的折中。

有界模型驗證（Bounded Model Checking），即使用SAT（Boolean satisfiability）求解器在一定邊界條件下尋找反例。

在實際應用中，業界也有一系列應對狀態爆炸問題的方法，我將在下一章進行詳細闡述。

如何使用形式化驗證

那么，應該如何著手使用形式化驗證？首先需要考慮如何將設計規約和需求用形式化的方法表述出來。

驗證的本質就是將設計與設計規約進行一一比對的過程。在電路仿真中，通常使用參考模型（reference model）作為設計規約的實現形式。參考模型通常由高級語言，如C/C++、SystemC、MATLAB等實現，但有時也會通過RTL語言如SystemVerilog實現。與此不同的是，在形式化驗證方法中，設計規約是通過形式化的語言進行抽象和描述的，而并不需要參考模型。具體而言，設計規約通常會被拆分成若干條“屬性”（Property），然后通過SystemVerilog斷言（SystemVerilog Assertion – SVA）來進行描述。

SVA是SystemVerilog語言的一個子集，其實它已然被廣泛用于傳統的電路仿真中，但使用范圍比較受限，主要用來檢查在仿真中某些狀態（通常為異常狀態）是否會發生。在形式化驗證中，SVA則是作為主要的編程語言，用來描述設計規約的各條屬性、對設計的行為進行建模、提供實際的約束、提取覆蓋率等等。

總體而言，SVA的層次可以根據所表達的復雜度分為如下四級：

1. 布爾運算（Booleans），如

data[0] && data[1] && data[2]

2. 序列（sequence），用來表達在一段時間內發生的一系列布爾運算。因此可見序列的表示需要一個明確的時鐘作為參考。例如：

req ##2 grant

這代表當req置一后再過兩個時鐘周期，grant再置一。

3. 屬性（property），用來組合多個序列，并以此表明在設計中需要滿足的某種邏輯關系。如：

A |-> B 和 A |=> B

其中A和B都為序列。本例中前者代表當A成立時，B在同一個周期內也必須成立；后者代表當A成立時，B在下一個周期必須成立。

4. 斷言聲明（assertion statements），用來表示對一則SVA屬性所進行的動作，例如：

p1: assert property (A |-> B);

這代表將對括號內的property進行斷言檢查。具體來講，斷言聲明通常使用以下三個關鍵詞之一：assert，assume和cover。這三個關鍵詞在形式化驗證環境中的語義和在電路仿真中有所不同：

Assert：用來表明給定的斷言聲明（statement）必須在任何條件下都滿足；

Assume：用來指定各種形式化驗證的約束條件

Cover：用來表明在形式化驗證的過程中必須要覆蓋到的情況

形式化驗證流程

由于篇幅所限，其他更深入的有關SVA的介紹和舉例無法在本文給出。有興趣的讀者可以查看相關的文獻書籍以了解更多。本文想強調的是，在形式化驗證中，各種設計規約、約束條件、驗證目標、覆蓋點等，都是通過SVA進行表述和建模的。這樣，可以把圖2中所示的簡單的形式化驗證流程圖擴展為如下圖所示：

圖8：擴展后的形式化驗證流程

由上圖和前圖的對比可以看到，形式化驗證引擎的輸入輸出都進行了一些擴展。在輸入端，除了在仿真中也需要的待測模塊以外，形式化驗證還需要對輸入進行一定的約束，并通過SVA的描述，提供待驗證的斷言和覆蓋點。

通常來講，使用形式化驗證的第一步，并非是立即編寫各種斷言，而是構思需要對整個設計和驗證環境添加怎樣的約束。形式化約束的意義在于能很大程度上的減小狀態空間，一方面能引導形式化驗證工具在更加合理的狀態區間中進行更有效的斷言判定，另一方面能夠從一開始就杜絕一些不合理的狀態或條件的出現，從而避免驗證出現漏報（false negative）。為形式化驗證添加約束還能“強迫”設計者和驗證工程師在整體上全面思考設計規約以及設計需求，從而在早期發現設計規約和需求中的漏洞和不足。

在明確各種約束條件之后，接下來需要考慮設計中存在哪些目標狀態，并通過覆蓋點進行覆蓋。這與使用隨機約束的驗證方法中，提取功能覆蓋率的思想比較類似。通常這些目標狀態都在驗證計劃中給出。需要注意的是，在形式化驗證中，覆蓋點還有一個重要作用是防止誤報（false positive）的出現。最極端的例子是，如果不給出任何斷言，那么形式化驗證工具就會給出全部斷言都被證明的誤報。因此需要覆蓋點對目標狀態進行覆蓋，確保工具對相關斷言的確進行了證明。

在形式化驗證工具的輸出端，通常會給出三類信息：

1.若斷言得到證明，則會給出已經被證明的斷言列表；

2.若斷言被證明有誤，則會給出一個反例（如上文所述通常為最小實例）；

3.若在有限時間之內，工具無法給出證明或反證，則會標明該斷言的證明沒有定論（inconclusive）。

有很多種可能性會導致出現最后一種情況，例如證明時間太短、斷言及屬性過于復雜等，但通常代表此時的狀態空間太大，已經超出了形式化工具可以證明的范圍。此時應該考慮著手減小狀態空間，例如考慮簡化斷言、提供更多約束、嘗試其他的形式化驗證引擎等。也可以使用更進一步形式化驗證技巧，如使用抽象模型（abstraction），設置黑盒（blackbox）或斷點（cut-point），對待測設計采用分而治之的策略等。

例如對于一個大小為32位寬、512個存儲單元的存儲器，理論上它的狀態空間存在2^(32*512)個狀態， 即大約十億的一千次方，已經遠超計算機可以計算的范圍。另一方面，對于存儲器本身而言，其通常作為一個可配置的IP使用，對于使用存儲器IP的設計而言，驗證存儲器自身的功能并非驗證的目的。而且，我們往往可以安全的假設，存儲器本身已經經過了IP提供商的完整驗證，可以直接使用。此外，可以注意到每個存儲器的存儲單元均相互獨立，很多情況下兩個存儲單元的內容并不會相互影響。

在這種情況下，我們可以使用針對存儲器的抽象模型，只對少數存儲單元進行精確建模，而不需關心其他單元，那么可以將整體的狀態空間下降為2^(32*3)個狀態。

對形式化驗證中的抽象模型的研究一直是業界和學界的熱點之一，比如，英國Imagination公司的Arshish Darbari等人曾經發表過多篇文章，詳細闡述了關于FIFO、Arbiter等模塊的形式化抽象方法。我的博士導師，倫敦帝國理工學院的Constantinides教授也曾對多項式數據通路的形式化驗證開展過一系列理論研究工作。形式化驗證咨詢機構Oski也發表過一系列文章，詳細講解了諸如如何對FIFO等底層模塊進行形式化抽象，如下圖所示。

圖9：Oski提出的FIFO形式化抽象方法

同時，形式化驗證工具的提供商，如Candence和Synopsys也都提供了一些常用模塊，如FIFO、存儲器、乘法器等的抽象模型。

綜上所述，一個較為完整的形式化驗證環境會如下圖所示。

圖10：一個形式化驗證環境示意圖

筆者眼中的現代驗證方法學

在筆者眼中，形式化驗證將在現代驗證方法學中慢慢占有越來越重要的地位。這主要是由于形式化驗證獨特的工作原理，及其先天優于基于電路仿真的驗證方法的各類特性。同時，形式化驗證適用于多種不同的模塊層級，從小規模的IP設計，到大規模的系統集成，都有可能使用形式化的方法進行驗證。很多業界的公司都早已開展形式化驗證的使用，比如英特爾就對其i7處理器的某核心部件全部使用形式化方法進行驗證。另外，隨著EDA工具的不斷完善，普通的使用者，如設計和驗證工程師，不需要掌握任何形式化理論或數學模型推導，這些過程都已被封裝在工具中，這樣大大簡化了形式化驗證的使用門檻。形式化驗證另一個主要的作用在于，能夠幫助設計者充分嚴謹的思考設計需求和規約，并在設計早期就能有效發現各類漏洞，而無需等待復雜的測試平臺搭建完成。

另一方面，如前文提到的，形式化驗證也伴隨著先天的缺點，即不能有效處理擁有大量狀態的設計，如存儲器、數學運算器等。為了應對這樣的情況，驗證工程師需要掌握一些形式化驗證技巧和抽象方法。此外，形式化驗證與電路仿真的思考角度完全不同，一個熟練使用UVM和隨機約束的驗證工程師不一定能在短時間內很好的掌握形式化驗證的思想和工作方法。這幾點都使得形式化驗證又不是那么簡單易用。

因此，業界的共識在于，充分利用形式化驗證和電路仿真的優點，揚長避短，在一個完整的項目周期內協同使用不同的驗證方法學。業界有關項目進行時間和漏洞數量關系、修復漏洞的花費三者關系的經驗圖如下所示，可見在項目開發初期，是各類漏洞存在的高發期，但此時修復漏洞所需要的成本最少。等到項目行將結束并流片的時候，漏洞很難被找到，但一旦出現就往往需要花費大量成本進行修復。

圖11：Bug數量、修復Bug的成本與所在的項目開發周期的關系

因此，在項目早期，可以利用形式化方法逐步完善設計規約，同時發現各類早期的問題和簡單的漏洞。設計者也可以負責編寫各類斷言，而驗證工程師負責形式化平臺的搭建，以及更復雜斷言的設計。與此同時，使用UVM等方法學搭建電路仿真平臺，用以在更高層次（如系統集成時）、和項目中后期通過不間斷的回歸測試發現設計漏洞。當基本測試完成后，可以使用硬件模擬和FPGA原型設計等方法，再進行大量實際數據的測試。特別是對基于FPGA系統的設計，由于FPGA的可編程性，有條件的話可以更早進行硬件測試。