一種智能網(wǎng)卡的形式驗證流程

介紹

這篇論文總體上不難理解，背景是開發(fā)智能網(wǎng)卡的團隊在驗證智能網(wǎng)卡IP過程中，由于需要考慮數(shù)量龐大的錯誤場景，而不得不在原本已經(jīng)啟動的隨機約束仿真驗證（CBRV）基礎(chǔ)上，添加了形式驗證（FPV），繼而在更短的時間里，找到了數(shù)量更多且更復(fù)雜的bug（好吧，形式驗證聽起來總是那么酷，屠龍術(shù)就是這么傲嬌）。

論文容易理解的一個特征在于它會把這篇論文的背景和相關(guān)知識交代得易于理解。就比如它在描述有哪些錯誤類型的時候，將系統(tǒng)錯誤逐一劃分，繼而一直到它接下來要處理的功能描述錯誤即specification violation errors，這類錯誤也屬于可檢測到的錯誤類型，并且需要由設(shè)計報告出來，并且在報告以后設(shè)計還能夠恢復(fù)正常。即在驗證這個智能網(wǎng)卡IP的過程中，不但需要關(guān)注功能正確，而且還需要特別關(guān)注它可能遇到的（幾乎所有）錯誤情況，并且設(shè)計要能夠?qū)⑦@些錯誤情況檢測（detect）、報告（report）出來，最后從錯誤狀態(tài)中恢復(fù)（restore）到一個可知狀態(tài)，在人為較少介入的情況下，還能夠繼續(xù)處理后續(xù)的數(shù)據(jù)包。

正由于本文智能網(wǎng)卡需要長期、頻繁處理大量數(shù)據(jù)，它就有很多種出錯的可能，而對于錯誤的處理就成了這個設(shè)計功能的一部分。這一點往往在很多其它設(shè)計中也有錯誤處理，但沒有本文IP的要求高。但在CBRV中，由于UVM環(huán)境中的組件在設(shè)計時往往并沒有充分考慮如何插入錯誤，這也使得讓充分測試發(fā)生錯誤場景的要求變得困難，而且還可能帶來較大的工作量。

提出問題

文中要驗證的是NIC（Network Interface Card） IP中的一個解壓縮IP，它的特點一如其它數(shù)據(jù)流處理的模塊，也是需要對數(shù)據(jù)幀、數(shù)據(jù)塊做數(shù)據(jù)接收、校驗、格式檢測等內(nèi)容，并就違反數(shù)據(jù)協(xié)議的有關(guān)問題進行識別和報告。如果是要驗證它的正常功能，那么就需要給它提供符合協(xié)議的經(jīng)過壓縮的數(shù)據(jù)。

為了加速驗證過程，在CBRV環(huán)境中他們采用的是軟件壓縮生成器（SW compressors），可以簡單理解為通過已有的（來自外部或者內(nèi)部的）軟件壓縮應(yīng)用來對原始數(shù)據(jù)進行處理，并生成壓縮后的數(shù)據(jù)文本，再將這些符合協(xié)議的數(shù)據(jù)通過協(xié)議激勵的形式發(fā)送給解壓縮IP，解壓縮IP如果處理妥當(dāng)?shù)脑?，那么最終識別解包的數(shù)據(jù)可以通過monitor采集下來，并且與原始數(shù)據(jù)（在交給軟件壓縮生成器之前的數(shù)據(jù)）做比較。這種方式比較流程是從文中給的描述方式推斷得出的。

只不過也正如文中談到的，這種方式適合驗證滿足壓縮數(shù)據(jù)協(xié)議的情況，但無法更好地解決一些驗證完備性的問題，它們包括：

使用的軟件壓縮生成器并不足夠靈活，只能生成協(xié)議中的一部分數(shù)據(jù)協(xié)議格式。

如果企圖去修改這些生成器似乎不那么容易做反向工程，因為有些協(xié)議中要求的部分被優(yōu)化掉了（也就失去了插入一些錯誤邏輯的可能）。

軟件壓縮生成器與壓縮協(xié)議是一致的，但本身（一般）不支持插入錯誤，更談不上錯誤的格式配置（因為這往往只有在硬件驗證的時候才需要，而軟件壓縮生成器只是為了做數(shù)據(jù)協(xié)議的通路驗證）。

基于此，可能需要在CBRV進行到一半的時候，再考慮是否需要就協(xié)議數(shù)據(jù)包的生成專門去做一個數(shù)據(jù)包生成器（例如由UVM來實現(xiàn)），但這也會在帶來額外的工作量，而且還需要考慮協(xié)議中的各種組合情況（CBRV本身不會去做窮舉組合，但目前有工具可以幫助做窮舉組合覆蓋率的收斂）。同時，也需要在實現(xiàn)協(xié)議driver的過程中就考慮在其中插入多個錯誤回調(diào)函數(shù)（從我們過去的實現(xiàn)經(jīng)驗來看這么做更加合理），以便于在sequence中通過綁定錯誤回調(diào)函數(shù)和錯誤類型來最終實現(xiàn)錯誤數(shù)據(jù)協(xié)議的插入。

但問題依然在，如果我們像AHB、I2C這些數(shù)據(jù)總線的錯誤協(xié)議，我們可以根據(jù)VIP的錯誤類型來選擇插入不同的錯誤（這些錯誤類型往往是根據(jù)對協(xié)議的理解由VIP（Verification IP）提供商考慮來實現(xiàn)的，但數(shù)據(jù)總線協(xié)議標準并沒有規(guī)定所有的協(xié)議錯誤的情形），而文中的解壓縮IP已經(jīng)對出現(xiàn)的各種錯誤可能都做了錯誤代碼劃分，也就是說它對功能錯誤的重視程度與功能正確的情況是一致的，我們需要驗證的是，該IP在【所有規(guī)定錯誤類型】的情況下，都能檢測（detect）、報告（report）錯誤并從錯誤中恢復(fù)（restore）正常。

這意味著即便我們花了大力氣去實現(xiàn)CBRV需要的可以做不同數(shù)據(jù)格式配置的一個滿足協(xié)議的driver，但還需要在driver內(nèi)部準備多處錯誤插入邏輯。從我們過去的實現(xiàn)經(jīng)驗來看，我們實現(xiàn)正常的協(xié)議邏輯從基本功能到復(fù)雜功能是在做加法，而在繼續(xù)實現(xiàn)插入錯誤的邏輯上面，我們可能是在做乘法。因為我們既要能夠?qū)崿F(xiàn)插入錯誤的功能，還要讓這個功能不會影響到原有的正常驅(qū)動功能，而且還別忘記，我們還要考慮monitor是否需要對這些錯誤進行分類監(jiān)測識別?？梢赃@樣說，這幾乎給我們帶來了至少雙倍的工作量。

總而言之，這種為了遍歷錯誤（也是一種功能測試要求）而去讓CBRV的環(huán)境更加完善（且投入更多人力）的考量，給本文作者他們帶來了一些新的選擇。他們試圖讓FPV也參與到驗證過程中來，繼而降低整體的工作量（我沒有見過他們的項目數(shù)據(jù)，就降低整體的工作量我持謹慎態(tài)度）和提高發(fā)現(xiàn)bug的效率。

解決方案

將這個解壓縮IP做結(jié)構(gòu)簡化的話，可以分為解碼邏輯（decode logic）、錯誤檢測+報告邏輯（error detection logic）和控制邏輯（包含錯誤恢復(fù)，control logic）。在形式驗證中，我們需要遵循一個基本原則就是簡化設(shè)計，或者說是簡化每一個斷言屬性要檢查的邏輯。這就要求我們在一開始就需要考慮將設(shè)計進行拆分，就拆分的邏輯部分分別做形式驗證，采取“分而治之”的方案，這個方案在數(shù)據(jù)流類型設(shè)計的形式驗證中經(jīng)常被采納。

于是他們給的方案是對錯誤的檢測、報告和恢復(fù)（控制）邏輯分別展開驗證。只不過實際上文中并沒有對形式驗證的覆蓋率給出數(shù)據(jù)，這也使得在最后與CBRV驗證做比較的時候，是針對bug發(fā)現(xiàn)情況做的比較。因為形式驗證的覆蓋率部分也能幫助指出整個完整數(shù)據(jù)通路是否可以通過形式驗證完成，即數(shù)據(jù)完整性（data integrity）的驗證，否則在文章最后就CBRV與FPV的比較維度就不夠完整，也無法讓我們放心是否有信心在今后的工作有可能只采用FPV，而完全擱置CBRV。要注意的是，本文是就CBRV與FPV在驗證流程和發(fā)現(xiàn)bug上的比較，但其實仍然隱去了一部分“工程現(xiàn)實”。而我談到的工程現(xiàn)實，卻可能決定了一個方案是不是能夠更可靠地去“落地”。

在介紹接下來的3種分而治之的驗證方案前，還需要清楚的是，實際的形式驗證工程實現(xiàn)并沒有下面簡化后的這樣“完美”，因為從本質(zhì)而言，形式驗證也對應(yīng)著“激勵”（stimulus）、“監(jiān)測”（monitor）和“比較”（check），只不過它是由斷言屬性的assume來實現(xiàn)了激勵、assert property的前置算子（sequence）實現(xiàn)了監(jiān)測以及assert property的后置算子(sequence）實現(xiàn)了比較。

比如下面的錯誤檢測驗證和錯誤報告驗證的兩種形式驗證子任務(wù)，就沒有就它們是如何構(gòu)建assume來做描述，以及如何在已滿足協(xié)議的多個assume中，添加多種錯誤的assume，繼而實現(xiàn)不同的錯誤可能這些工程實現(xiàn)進行描述。要知道協(xié)議往往越復(fù)雜，那么構(gòu)建一組滿足協(xié)議的assume，以及基于這些assume再添加引起錯誤的assume，都需要經(jīng)驗。只不過，相比于CBRV實現(xiàn)的driver中軟件處理邏輯，F(xiàn)PV中的assume要更偏向于粒子化（atomic），也因此我們要插入一種錯誤，更容易與原有的assume組進行融合，無外乎是disable某些assume，再引入某些引起特定錯誤類型的assume。

最糟糕的情況可能是不對輸入數(shù)據(jù)的協(xié)議做任何assume規(guī)范，但這對于前期穩(wěn)定設(shè)計、調(diào)試設(shè)計都有顯著的不利影響，這屬于過于寬松的約束。往往是在設(shè)計穩(wěn)定（測試過大多數(shù)正常功能）以后，我們才開始將約束逐步放寬，而我們這里說的約束寬松或者收窄，在CBRV或者FPV中都有這樣的激勵原則。 因此請在閱讀本論文有關(guān)如何實現(xiàn)這三部分設(shè)計邏輯的形式驗證時，理解論文作者為此做的抽象和簡化，懂得“理想和生活往往只有一步之遙”的距離那么遠又那么近... ...

錯誤檢測驗證

在這部分里，作者對解壓縮IP需要處理的多種錯誤類型做了一個歸類展示以說明他們需要就這些錯誤可能在FPV過程中都激勵到。

就比如舉的一個例子，要檢測數(shù)據(jù)塊的最大size，可以通過簡化后的2個斷言來實現(xiàn)“有且只有”的該錯誤類型的檢查。但要注意的是，下面斷言中使用的變量block_size從何而來，如果來自于設(shè)計內(nèi)的信號，那么就還需要就該信號的邏輯做補充驗證。這種規(guī)則也符合我們談到的“分而治之”的理念，即如果你需要按照灰盒去降低形式驗證的復(fù)雜度，那么你就需要對使用的設(shè)計變量做補充驗證，證明它們的邏輯正確。

在下面的例子中，就需要證明block_size信號跟設(shè)計端口接收到的數(shù)據(jù)有關(guān)，且是經(jīng)過數(shù)據(jù)包拆分后得到的邏輯。這部分邏輯往往可以在形式驗證中也采用always/task這樣的“膠水”邏輯做補充處理，繼而證明block_size的邏輯正確。當(dāng)然，下面的例子我們也可以直接采用經(jīng)過膠水邏輯處理后的變量。兩種方法，第一種是灰盒驗證式的（采納部分設(shè)計變量），第二種是黑盒驗證式的（全部采用自有變量）。

錯誤報告驗證

既然能夠檢測出錯誤，那么將錯誤正確無誤地歸類并且將8位的錯誤碼發(fā)送出去，就屬于錯誤報告的驗證部分了。

在下面簡化后的代碼中可以看到，只要錯誤能夠檢測出來（我們對這一步仍然做假設(shè)，可以利用設(shè)計中的變量，采取灰盒驗證），就能夠投入到錯誤報告的驗證當(dāng)中。在設(shè)計中，要歸類這些錯誤類型，也往往會有可以直接使用的error flag變量，再結(jié)合輸出端口的錯誤代碼，即能夠?qū)@些錯誤報告做驗證。

這部分代碼顯然可以復(fù)用，即當(dāng)我們給入不同的error flag變量和對應(yīng)的錯誤類型代碼時，我們就可以同時驗證256個錯誤類型。只不過形式驗證不需要我們采用CBRV的方式去窮舉這個256個test case，而只要我們的激勵環(huán)境具備這個能力（assume group需要能夠支持產(chǎn)生錯誤激勵，且同時有條件出發(fā)不同的錯誤類型）。

在這種情況下，我們不必像CBRV為了每個test case去考慮支持插入的錯誤類型，要注意這些錯誤類型甚至都無法由某一個錯誤幀構(gòu)成，可能是多個錯誤幀共同影響下的產(chǎn)物，F(xiàn)PV毫無疑問降低了為此我們要不斷更新driver的壓力。我們只需要讓assume group能夠自洽地去有條件產(chǎn)生一些我們想得到的和沒有想到的激勵，繼而讓它們?nèi)ビ|發(fā)一些錯誤類型，并且去滿足給定的錯誤類型斷言。

可以預(yù)見到的是，錯誤類型斷言未必都能夠得到檢查，即空成功（vacuous success），即這些沒有被觸發(fā)前置條件的錯誤斷言類型由于我們給定的assume過約束（over constraint）而沒有被觸發(fā)檢查。在這種情況下，我們往往需要多個任務(wù)場景，構(gòu)建多種assume group，才能最終將這么多的錯誤類型都做到覆蓋。

控制恢復(fù)邏輯驗證

智能網(wǎng)卡對于能夠從數(shù)量眾多的錯誤中恢復(fù)正常數(shù)據(jù)處理的要求很高，這也使得在本文中的解壓縮IP驗證中，需要在錯誤檢測和報告之后，仍然需要確保設(shè)計功能能夠恢復(fù)正常。

例如給出的這個簡化后的狀態(tài)機，既需要考慮是否所有的狀態(tài)都已經(jīng)遍歷，而且也要在遍歷之后檢查設(shè)計功能是否正常。對于狀態(tài)機的測試，在CBRV層面如果不受額外的人工介入，那么覆蓋率將會在到達某個階段后緩慢爬坡。而如果人工需要介入，那么就還需要考慮設(shè)計特定的測試場景去觸發(fā)那些沒有覆蓋到的狀態(tài)跳轉(zhuǎn)情況。

往往狀態(tài)機越復(fù)雜，用來分析狀態(tài)機的難度就越大，用來單獨設(shè)計為增加跳轉(zhuǎn)覆蓋率的測試用例就越難以把控。這里測試用例激勵難以把控的原因是，這些激勵需要通過若干不同的時序和邏輯處理后，才有機會去觸發(fā)狀態(tài)機的跳轉(zhuǎn)，但這種跳轉(zhuǎn)不是能夠做到100%出現(xiàn)的。

那么當(dāng)這些錯誤狀態(tài)越多，解壓縮IP的錯誤恢復(fù)控制邏輯測試對于CBRV的要求就越高，不但需要創(chuàng)建指定場景（有時這種場景都未必容易造出來），還需要在這些測試中關(guān)注每一種特定的狀態(tài)跳轉(zhuǎn)事件，繼而觸發(fā)某些信號用來收集覆蓋率。

對于熟悉CBRV驗證的朋友來說，如何去讓狀態(tài)機提高它的跳轉(zhuǎn)覆蓋率本身就不是SV/UVM能夠直接起作用的，目前EDA公司也在推他們的有關(guān)“智能收斂”的方案，往往會跟他們的回歸工具和仿真器做綁定，如果你們公司有精力做這樣的嘗試，可以試著聯(lián)系EDA廠商的AE，試著在你們的環(huán)境中找個piolot項目先做做看，評估一下是否便于落地。

說回到FPV的驗證方案，那就是考慮就這部分控制邏輯做單獨驗證，因為從激勵的角度來看，你的激勵距離目標越近，那么就更容易控制、觸發(fā)目標設(shè)計中的邏輯，也就是去提高狀態(tài)機的各種跳轉(zhuǎn)覆蓋率。如果就CBRV而言，這種方式不是一個常規(guī)方式，因為CBRV的環(huán)境里如果這部分control logic處于設(shè)計內(nèi)部，那么設(shè)計內(nèi)部的邏輯驅(qū)會驅(qū)動它，這種傳導(dǎo)關(guān)系要求我們?nèi)匀粡脑O(shè)計端口給激勵。當(dāng)然，我們也可以采用“侵入式”（invasive）激勵，直接將激勵數(shù)據(jù)灌入到內(nèi)部設(shè)計的邊界，只不過這種方式還需要改造UVM環(huán)境，畢竟它不是仿真環(huán)境原生支持的。

對于形式驗證工具，它可以通過先切斷（cut-point）設(shè)計中的驅(qū)動邏輯，再將目標變量的驅(qū)動交由assume property去做激勵的形式，靈活地將激勵從解壓縮IP外部送入，同時將一部分激勵直接給入到需要驗證的control logic部分。在這種情況下，F(xiàn)PV可以更直接地去對control logic模塊做激勵，并且收集它的信號。這部分額外的assume/assert property可以通過單獨的模塊bind到這部分control logic模塊。

從上面簡化的代碼來看，就單獨測試狀態(tài)機而言形式驗證的窮舉模式會更有效，但也別忘記，我們?nèi)匀恍枰プC明所接管control logic的error signal功能（已由錯誤報告驗證方案完成），以及它的輸出控制信號最后對設(shè)計恢復(fù)正常功能的作用。

未提及的FPV部分

本文將三部分邏輯的功能和聯(lián)系講清楚了，盡管有較多的簡化，但總體的功能邏輯是清晰的。只不過在接下來的總結(jié)部分，并未提及覆蓋率的部分，無論是代碼覆蓋、斷言覆蓋率還是功能覆蓋率。而且，還有重要的一點是，F(xiàn)PV的驗證方案只做了“切分”和“簡化”，但未提及對于整體數(shù)據(jù)通路的數(shù)據(jù)完整性驗證。

要知道，如果沒有這部分驗證，那么我們肯定是對于FPV以后做獨立完備性驗證缺少信心的。但由于本文做了對比驗證，那么CBRV部分的整體數(shù)據(jù)通路驗證是完成的，也因此從項目上降低了對FPV的要求。也就是說，可以利用FPV的靈活性和窮舉能力，讓它更多地舉出反例，幫助找到一些考慮不到的bug。往往是由于FPV的窮舉能力，也就能夠幫我們觸發(fā)更多違例（violation）場景，挖掘到一些我們沒有注意到的測試盲區(qū)并找到bug。

總結(jié)

一般形式驗證的論文都會將FPV所發(fā)現(xiàn)的bug與CBRV做比較以此來證明它們“打掃全屋無死角”的能力，這對于開發(fā)IP確實很重要。那反過來看，如果IP驗證時只采用了CBRV，而沒有采用FPV的話，是不是意味著有很多“隱秘的角落”沒有被訪問過，手機前的你如果在做IP驗證的話，是不是驚起了一身冷汗？

而從驗證效率來看，F(xiàn)PV的收斂速度也較CBRV有明顯提升，往往在設(shè)計75%測試點完成度上面，F(xiàn)PV使用了12周，而CBRV使用了28周的時間，也就是整整快了16周的時間（4個月，天啊，好奢侈的時間裕度）。不過從論文的描述來看，CBRV的環(huán)境是先行的，對于設(shè)計的理解和趟的坑也給后面開展FPV提供了提速條件。我推測做FPV和CBRV的人應(yīng)該是同一批，他們一邊做一邊也在交叉記錄和比較。

在最后的展望階段，文章作者還預(yù)計要將這部分錯誤處理的經(jīng)驗帶入到SoC驗證上面，我倒是對他們準備如何展開SoC層面的分而治之的方案很感興趣，不過相比之下我可能對于PSS的系統(tǒng)測試場景構(gòu)建能力更有信心哦。

審核編輯：劉清