介紹

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

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

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

提出問題

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

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

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

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

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

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

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

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

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

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

解決方案

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

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

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

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

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

錯誤檢測驗證

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

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

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

錯誤報告驗證

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

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

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

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

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

控制恢復邏輯驗證

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

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

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

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

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

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

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

從上面簡化的代碼來看，就單獨測試狀態機而言形式驗證的窮舉模式會更有效，但也別忘記，我們仍然需要去證明所接管control logic的error signal功能（已由錯誤報告驗證方案完成），以及它的輸出控制信號最后對設計恢復正常功能的作用。

未提及的FPV部分

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

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

總結

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

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

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

審核編輯：劉清