回顧集成電路的未來的分析介紹

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

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

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

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

什么是形式化驗證

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

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

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

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

形式化驗證的主要優(yōu)點

與傳統(tǒng)的基于仿真的驗證方法相比，形式化驗證主要有以下三個方面的優(yōu)點。

第一，形式化驗證能覆蓋完整的設(shè)計狀態(tài)空間。

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

電路復(fù)位后的初始化狀態(tài)， 也稱為復(fù)位狀態(tài)；

內(nèi)部邏輯實現(xiàn)時的中間狀態(tài)；

各個輸入輸出的狀態(tài)。

比如，在一個FIFO設(shè)計中，它的“滿”、“空”指示就是輸出的狀態(tài)；在某一時刻，F(xiàn)IFO里內(nèi)存的讀寫指針的位置就是中間狀態(tài)；而當(dāng)復(fù)位完成后，指針位置以及當(dāng)時“滿”、“空”指示的值就是復(fù)位狀態(tài)。

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

在電路仿真中，每次仿真實際上就是在狀態(tài)空間里尋找一條從“復(fù)位狀態(tài)”到“輸出狀態(tài)”的路徑， 如下圖中標(biāo)出的一條路徑。

圖3：一次仿真得到的狀態(tài)路徑

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

圖4：多次仿真得到的狀態(tài)路徑

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

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

圖5：形式化驗證對狀態(tài)空間的全覆蓋

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

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

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

圖6：形式化驗證可以提供到達(dá)目標(biāo)狀態(tài)的最小實例

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

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

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

3. 無法確定是否還有其他條件能夠達(dá)到目標(biāo)狀態(tài)。

和電路仿真不同，形式化驗證可以很快的給出達(dá)到目標(biāo)狀態(tài)的最小實例，或者反之，得出結(jié)論證明該目標(biāo)狀態(tài)永遠(yuǎn)不會被達(dá)到。電路設(shè)計者和驗證者可以通過這個特性，利用形式化驗證對目標(biāo)狀態(tài)進(jìn)行快速調(diào)試，并通過給出的最小實例，更好的理解電路行為，及時發(fā)現(xiàn)其與設(shè)計規(guī)約的偏差。

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

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

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

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

圖7：形式化驗證可以進(jìn)行基于狀態(tài)或輸入的調(diào)試和驗證

形式化驗證的主要缺點

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

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

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

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

基于反例的抽象優(yōu)化（counterexample-guided abstraction refinement），即自適應(yīng)的尋找合適的抽象層次，實現(xiàn)精度和運行時間的折中。

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

在實際應(yīng)用中，業(yè)界也有一系列應(yīng)對狀態(tài)爆炸問題的方法，我將在下一章進(jìn)行詳細(xì)闡述。

如何使用形式化驗證

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

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

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

總體而言，SVA的層次可以根據(jù)所表達(dá)的復(fù)雜度分為如下四級：

1. 布爾運算（Booleans），如

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

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

req ##2 grant

這代表當(dāng)req置一后再過兩個時鐘周期，grant再置一。

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

A |-> B 和 A |=> B

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

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

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

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

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

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

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

形式化驗證流程

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

圖8：擴(kuò)展后的形式化驗證流程

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

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

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

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

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

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

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

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

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

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

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

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

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

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

圖10：一個形式化驗證環(huán)境示意圖

筆者眼中的現(xiàn)代驗證方法學(xué)

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

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

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

圖11：Bug數(shù)量、修復(fù)Bug的成本與所在的項目開發(fā)周期的關(guān)系

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