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

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

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

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

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

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

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

深圳市麗晶微電子科技有限公司，專注于太陽能閃燈IC，太陽能充電IC，太陽能控制器IC方案，太陽能草坪燈控制IC，太陽能路燈控制器IC，太陽能草坪燈IC，太陽能草坪燈驅動IC,太陽能草坪燈芯片，太陽能充電管理IC，太陽能充電芯片，太陽能控制芯片，太陽能電池充電芯片，太陽能充電控制芯片，太陽能LED燈串驅動芯片。