一、什么是形式驗證?

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

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

圖1. 形式驗證概念圖

1. reference design 和 implementation design

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

2. logic cone和compare point

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

圖2. 設(shè)計的邏輯錐劃分

3. Consistency and Equality

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

4. container和library

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

圖3. Container 和 library關(guān)系圖

三、形式驗證的基本流程

使用formality做形式驗證的基本流程如圖4所示，1)Load guidance階段是formality提取SVF文件信息的階段;2)接下來讀入設(shè)計，如果set_top聲明的設(shè)計頂層和待驗證的設(shè)計不是同一層次，需要使用命令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是不相同的，使用者在查看相應(yīng)命令的man page時需要注意。打開工具默認進入setup mode，執(zhí)行了math命令后進入match mode，執(zhí)行了verify命令后進入verifymode，而guide mode不易察覺，因為SVF信息的提取雖然在這一mode下進行，但是提取后工具又進入setup mode了，所以使用者不以察覺。

圖4. formality 應(yīng)用基本流程圖

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

審核編輯：湯梓紅