形式驗(yàn)證入門之基本概念和流程

一、什么是形式驗(yàn)證?

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

二、使用formality做形式驗(yàn)證需知的基本概念。

圖1. 形式驗(yàn)證概念圖

1. reference design 和 implementation design

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

2. logic cone和compare point

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

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

3. Consistency and Equality

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

4. container和library

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

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

三、形式驗(yàn)證的基本流程

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

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

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

審核編輯：湯梓紅