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

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

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

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

什么是形式化驗(yàn)證

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

圖2：形式化驗(yàn)證簡(jiǎn)要流程圖

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

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

形式化驗(yàn)證的主要優(yōu)點(diǎn)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

第二，形式化驗(yàn)證能提供最小實(shí)例

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

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

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

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

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

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

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

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

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

例如，在基于狀態(tài)的方法中，我們希望知道在一個(gè)設(shè)計(jì)中是否能夠通過(guò)某種方式達(dá)到某種狀態(tài)（如前文中所述），或者更進(jìn)一步，希望將此狀態(tài)作為接下來(lái)分析和調(diào)試的起始狀態(tài)。可以想象，使用電路仿真達(dá)成這樣的目標(biāo)很難，因?yàn)樾枰日业胶线m的輸入、經(jīng)過(guò)漫長(zhǎng)的仿真時(shí)間后才可能達(dá)到該狀態(tài)，而往往對(duì)于固定的輸入只會(huì)得到固定的輸出，如下圖所示。

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

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

形式化驗(yàn)證的主要缺點(diǎn)

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

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

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

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

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

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

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

如何使用形式化驗(yàn)證

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

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

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

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

1. 布爾運(yùn)算（Booleans），如

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

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

req ##2 grant

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

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

A |-> B 和 A |=> B

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

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

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

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

Assert：用來(lái)表明給定的斷言聲明（statement）必須在任何條件下都滿(mǎn)足；

Assume：用來(lái)指定各種形式化驗(yàn)證的約束條件

Cover：用來(lái)表明在形式化驗(yàn)證的過(guò)程中必須要覆蓋到的情況

形式化驗(yàn)證流程

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

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

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

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

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

在形式化驗(yàn)證工具的輸出端，通常會(huì)給出三類(lèi)信息：

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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