北冥草 路科驗證
隨着硬件設計復雜性的不斷增加，為了能夠最大程度的使得驗證收斂，驗證方法也越來越多，今天我們針對常見的幾種驗證方法做一些簡單的分析，指出它們的常用應用環境以及一些優缺點，主要包含：邏輯仿真，形式驗證，硬件仿真。
一、邏輯仿真
從我們整個芯片的驗證過程來講，基於軟件的邏輯仿真在驗證中仍然起着舉足輕重的作用，整個項目中的功能驗證都是通過邏輯仿真來進行驗證，下面我們就邏輯仿真的優缺點進行一個簡單的闡述：
優點：
-
邏輯仿真的工具可以在標准的服務器上運行，不需要為它定制特定的服務器，減少了驗證成本
-
在模塊級別的功能驗證上，邏輯仿真工具的編譯速度和仿真速度很快，這在一定程度上會加快我們整體項目的驗證速度
-
工程師對邏輯仿真驗證過程的進行有很好的控制，可以隨時暫停或者中斷驗證工具的運行，還可以以用戶友好的GUI模式來進行debug，提高了debug的效率
-
驗證環境的方便性，由於是基於軟件仿真，我們的驗證環境可以進入到DUT的任何一個需要被驗證的地方，在特定時刻產生足夠精確的數據包，進行仿真驗證
缺點：
-
對於邏輯仿真，上面的很多優點讓它在我們的驗證過程中充當着主力角色，但是它有一個很大的缺點，那就是性能，尤其是當我們的設計文件比較大時，邏輯仿真速度會變得很慢，這讓我們的驗證速度大打折扣，這也是我們后來引入形式驗證和硬件仿真的原因（以前我們只在整個SOC設計上應用硬件仿真，現在硬件仿真更早的被加入驗證過程）
二、形式驗證(屬性檢查和等價檢查)
形式驗證是一種靜態的驗證方式，旨在通過工具來從邏輯上來檢查我們的設計文件滿足/不滿足某種屬性，或者兩個設計文件是否邏輯等價
優點：
-
形式驗證是一種綜合性的驗證方式，我們可以設定一些屬性，它會以一種嚴密的邏輯方式窮盡所有可能去嘗試着證明我們的設計滿足/不滿足這種屬性，不像我們的邏輯仿真存在一定的概率性，因為在邏輯仿真中我們不可能窮盡所有的可能去驗證（可能要花費數年甚至幾十年去窮盡所有可能），但形式驗證可以做到而且往往只需要幾十分鍾或者數個小時
-
現在，形式驗證現在可以應用在跨時鍾域CDC(Clock Domain Crossing)驗證，在CDC驗證中，它可以識別CDC區域並進入電路中任何一個同步邏輯塊中，建立CDC的穩定性模型並用於RTL的仿真中以確認沒有這種不穩定的狀態穿過Clock Domain的邊界在DUT中繼續進行傳播；覆蓋率收斂方面，形式驗證也可以發揮很大作用，現在在我們的設計中會集成許多可配置可復用的設計模塊，但是由於配置方式的不用，使得它的功能不同，覆蓋率也就很難打到我們的要求(通常為100%)，形式驗證可以根據對模塊的配置做一個覆蓋率的分析，如果可以覆蓋，它會給出一個覆蓋的例子，如果不可以那我們就需要高度重視去重新檢查可不可以過濾掉
缺點：
-
形式驗證一個很大的缺點是你不可以仿真DUT的一些動態行為，從它的工作遠原理來講，它是把我們的當前設計和一些標准的VIP（也可以是其他形式）來進行邏輯對等檢查，並不能對於動態行為進行驗證，所以形式驗證的結果完全取決於我們提供的VIP的質量，如果VIP的質量很高，那我們的設計也沒有問題，反之則不行，也正式因為這個原因使得它不能作為驗證的主力軍
-
形式驗證的另一個比較大的缺點是隨着設計復雜性的增加，需要對比的DUT的狀態空間呈爆炸性增長，這使得形式驗證更多的應用在模塊級別，極大的限制了它在系統級別的應用
三、硬件仿真(Hardware Acceleration)
硬件仿真是指把我們的設計代碼進行編譯，並且綜合為真實的硬件電路對應FPGA板子上去，通過真實的硬件電路進行仿真(FPGA原型)
優點：
-
仿真速度快，對於我們的DUT來講，邏輯仿真工具的仿真速度大都在1KHz左右，通過用軟件的虛擬核代替硬件核仿真速度可以達到1MHz，而FPGA原型卻可以達到10MHz，利用硬件仿真，可以讓我們提高驗證速度，縮短驗證的時間，讓集成電路的發展沿着摩爾定律繼續前進
缺點：
-
編譯時間比較長，由於硬件仿真需要對設計文件進行邏輯綜合並且把綜合的結果對應到真實的硬件電路上去進行仿真加速，而對於基於軟件的邏輯仿真卻並不需要邏輯綜合生成物理電路，這就使得它的編譯時間相對邏輯仿真會很長
-
debug方式不是特別成熟，如果是一些比較容易發現的bug，可以借助硬件仿真進行，如果bug比較復雜仍然需要借助邏輯仿真工具進行，這使得硬件仿真速度很快，而debug又要回到慢速的邏輯仿真上面去，不能最大限度的發揮硬件仿真的速度優勢
總結
隨着驗證技術的發展，邏輯仿真在驗證中的使用變得越來越少，形式驗證和硬件仿真正在一步步更早的踏入驗證的的流程，發揮各自的作用，面對越來越復雜的硬件設計，僅僅用一種驗證方式去做到驗證收斂變得越來越困難，我們要結合各種驗證方法一起來對硬件設計進行各個方面的檢驗，讓我們的設計產品以很完美的姿態去完成它的使命。