一、什么是形式驗證?

VLSI設計的功能驗證有兩種方法，動態仿真驗證和形式驗證。形式驗證采用數學方法來比較原設計和修改設計之間的邏輯功能的異同，而動態仿真驗證是對兩設計施加相同的激勵后，觀測電路對激勵的反應異同。設計越大，為了達到100%的覆蓋率，動態仿真驗證所需要的矢量越多，這時形式驗證在這方面就有優勢了。但形式驗證是一種功能等價驗證，這種驗證脫離工藝和版圖約束，無法保證時序的準確性，故而，形式驗證往往需要和靜態時序分析工具一起來完成對電路完備的驗證。本文就以Synopsys公司的formality工具為例，來介紹形式驗證的流程和基本概念，后續會詳細介紹使用formality做RTL2Gate流程中每一步驟的操作。

二、使用formality做形式驗證需知的基本概念。

圖1. 形式驗證概念圖

1. reference design 和 implementation design

reference design是golden design，即認為是正確的標準的設計。implementation design是經過非功能性修改的、待驗證的設計。比如，使用綜合工具DC將RTL代碼映射成和工藝庫相關的門級網表，那么原RTL設計就是reference design，而DC輸出的門級網表就是implementation design。

2. logic cone和compare point

邏輯錐(logic cone)是由設計中的組合邏輯電路組成的，每個邏輯錐可以有多個輸入，只有一個輸出。邏輯錐的輸入為：設計輸入端口、寄存器輸出端口、黑盒子輸出端口;邏輯錐的輸出為：設計的基本輸出端口、寄存器輸入端口和黑盒子輸入端口。邏輯錐的輸出點就是比較點，reference design中的比較點和implementation design中的比較點是要一一對應的，這稱為比較點匹配(match)。Formality將設計劃分成一個個邏輯錐，以邏輯錐為單位，將其抽象為數學模型，然后針對每個比較點將implementation design和reference design進行比較，注意邏輯錐之間是可以交疊的。

圖2. 設計的邏輯錐劃分

3. Consistency and Equality

對于某個輸入pattern，reference design中某個比較點的響應為x，即0或1都可以的一個狀態，那么在implementation design 中相應比較點處的響應為0或者1，驗證都會通過，這叫做Design Consistency;而此時Design Equality要求在implementation design 中相應比較點處的響應也應該為x?？梢?，Design Equality的驗證標準要高于Design Consistency，對這兩種驗證，Formality工具都是支持的。

4. container和library

在Synopsys工具中，container是個常見概念，它就是一個存儲空間，formality中的container內存儲的是工藝庫和設計庫信息。通常，為了對兩個設計進行比較，我們需要將reference design放到一個container中，將implementation design放到另一container中。一旦啟動formality，工具會自動創建一個名為FM_WORK的工作空間，在這個工作空間里，默認創建了名為i和r兩個container，這兩個默認的container用起來很方便，當然，用戶也可以創建新的container。在向container中讀入設計的時候，如果不指定設計庫的名稱，formality會默認創建一個名為WORK的設計庫，并將設計讀入其中。在讀工藝庫的時候，如果不指定container，那么這些工藝庫會放到FM_WORK工作目錄下，并對所有container可見，稱為共享庫;如果指定了container，那么這些工藝庫會放到相應的container中，庫信息只能該container內部訪問。這樣，如圖所示，每一個design和design object可以通過container、design library、design、design object找到，這條路徑就是designID或objectID。

圖3. Container 和 library關系圖

三、形式驗證的基本流程

使用formality做形式驗證的基本流程如圖4所示，1)Load guidance階段是formality提取SVF文件信息的階段;2)接下來讀入設計，如果set_top聲明的設計頂層和待驗證的設計不是同一層次，需要使用命令set_reference_design和set_implemetation_design來聲明target design;3)在setup階段提供幫助比較點匹配的信息，聲明約束信息。4)match階段進行比較點匹配，這一步驟formality進行邏輯錐劃分、比較點映射和對讀入的SVF文件的信息處理(即guide命令處理);5)進行等價性驗證，若不一致需要debug。在整個過程中，涉及到四種shell mode：setup mode、match mode、verify mode和guide mode，每種mode下可使用的formality command是不相同的，使用者在查看相應命令的man page時需要注意。打開工具默認進入setup mode，執行了math命令后進入match mode，執行了verify命令后進入verifymode，而guide mode不易察覺，因為SVF信息的提取雖然在這一mode下進行，但是提取后工具又進入setup mode了，所以使用者不以察覺。

圖4. formality 應用基本流程圖

小結：本文介紹了形式驗證的基本概念和基本流程，有興趣的同學歡迎關注接下來對各個步驟的詳細介紹：如何恰當使用guidance、load design注意事項、setup階段需要補充哪些信息、比較點匹配規則和verify失敗時基本的debug方法等。

審核編輯：湯梓紅