眾所周知，驗證任務(wù)在數(shù)字IP的設(shè)計以及SoC的設(shè)計中占有重要地位。 RTL代碼和功能覆蓋率的目標(biāo)是達(dá)到100％，從而最大限度地縮短獲得它的時間。最廣泛使用的方法是基于通用驗證方法（UVM）隨機約束測試（系統(tǒng)Verilog或 e 語言），允許在相對短的時間內(nèi)構(gòu)建復(fù)雜的測試，同時強調(diào)RTL代碼和跟蹤功能覆蓋。一些驗證工程師還使用正式的方法來驗證塊的專用部分，例如標(biāo)準(zhǔn)接口，從而完成IP的驗證。

本文將介紹基于正式方法的數(shù)字IP驗證的不同方法，通過定義屬性詳盡地驗證功能。正式方法具有避免開發(fā)測試臺的優(yōu)點。這一新流程已在數(shù)字IP設(shè)計過程中使用，并已證明可顯著縮短驗證時間。

通用驗證流程

目前，用于驗證數(shù)字IP和片上系統(tǒng)（SoC）的最常用流程是基于UVM，通過使用第三方提供的驗證組件（VC）或非標(biāo)準(zhǔn)時從頭開發(fā)使用協(xié)議。然后用記分板完成測試平臺以進(jìn)行自我數(shù)據(jù)檢查，斷言用于驗證設(shè)計的特定部分，覆蓋用于跟蹤功能覆蓋。在過去幾年中，正式驗證已經(jīng)開始用于SoC和IP的驗證流程。在SoC中，形式驗證在SoC外圍設(shè)備和焊盤之間的連接驗證中變得非常普遍，主要是當(dāng)多路復(fù)用方案由連接到減少數(shù)量的焊盤的多個外圍設(shè)備形成時，這增加了需要驗證的組合。有時，在IP驗證中，正式方法用于檢查總線協(xié)議接口和寄存器訪問策略。

現(xiàn)在，關(guān)注數(shù)字IP的驗證，我們可以總結(jié)如圖所示的流程1.當(dāng)?shù)谝话鍾TL準(zhǔn)備就緒時，良好驗證流程的第一步從驗證和測試計劃的定義開始。在這個階段，我們將定義我們想要檢查的功能和測試的框架。

下一步是開發(fā)UVM測試臺;自定義UVM塊用于檢查特定的IP功能，而第三方UVM VC則實例化并綁定在RTL上。

此時，我們可以根據(jù)驗證計劃開發(fā)UVM測試。每個驗證工程師需要牢記的第一件事是測試必須是自我檢查;必須使用記分板，檢查器和斷言自動檢查驗證計劃中列出的任何點。然后，廣泛使用覆蓋結(jié)構(gòu)可以量化測試的好壞。

圖1：數(shù)字IP的通用驗證流程

有時，此流程可能包括形式驗證。在任務(wù)的某個階段，有人可能決定通過使用基于斷言的驗證IP（ABVIP）和通過編寫斷言通過有限狀態(tài)機（FSM）實現(xiàn)的精確功能來檢查IP的特定塊，例如總線協(xié)議接口。

我們知道，驗證任務(wù)是一個迭代過程，有兩個主要的環(huán)回：

RTL錯誤修復(fù)

功能和代碼覆蓋

每當(dāng)我們發(fā)現(xiàn)功能規(guī)范與IP行為不匹配時，我們就會向設(shè)計人員發(fā)出可能的錯誤信號。這意味著需要修改RTL并發(fā)布新的固定版本。現(xiàn)在，進(jìn)行回歸自檢測試（即使最初是部分測試）也是一個關(guān)鍵點，它允許我們驗證RTL代碼沒有回歸，當(dāng)然，錯誤已經(jīng)修復(fù)。這種環(huán)回也可以來自形式驗證。

當(dāng)開發(fā)了足夠數(shù)量的測試時，測量功能和代碼覆蓋率是一個很好的做法。像往常一樣，功能和代碼的目標(biāo)是100％，但我們必須考慮到達(dá)它的時間。如果我們想要最小化時間，同時保持100％的目標(biāo)，我們必須改進(jìn)驗證的方法和流程。來自正式世界的一個好建議是代碼不可達(dá)性分析，它有助于發(fā)現(xiàn)無法訪問的RTL部分，并且可以從整體代碼覆蓋率中刪除。

一個好的經(jīng)驗法則：'如果我沒有運用代碼的一部分，很可能是那里存在錯誤。'因此，我們花了很多時間才能刺激未覆蓋的代碼，但知道某個部分無法訪問可以讓我們節(jié)省時間和精力。

接下來，我們將描述一個新的流程，其主要目標(biāo)是縮短用于驗證數(shù)字IP的時間。保持覆蓋目標(biāo)。

新的驗證流程

正式方法是一種詳盡的驗證，當(dāng)它是適用時，它使人們能夠在更短的時間內(nèi)和每種可能的條件下檢查塊的功能。對于常見的動態(tài)模擬，這有時是不可行的。

目前，有幾種工具可以鏈接到正式引擎，這些工具已經(jīng)足夠成熟，可以使圖1所示的驗證流程變?yōu)槿鐖D2所示的內(nèi)容。 。

主要的變化是將形式驗證作為流程的第一步。真正的第一個檢查是對死代碼和未初始化寄存器的分析。這是一項零工作任務(wù)，因為不需要額外的代碼，并且它只需要使用Formal工具編譯RTL。隨后的反饋可能非常有用，因為它可以讓我們徹底清理RTL代碼，突出顯示從未到過的部分，以及列出可能導(dǎo)致'X'傳播的未初始化觸發(fā)器

毫無疑問，通過使用專用的基于斷言的VIP（ABVIP），可以在短時間內(nèi)完全驗證諸如微處理器總線接口之類的標(biāo)準(zhǔn)協(xié)議。 Formal流的這些驗證組件基于描述協(xié)議的斷言。驗證工程師將專注于失敗屬性的調(diào)試，而無需花時間在測試平臺和房地產(chǎn)開發(fā)上。通過使用UVM流，我們可以在幾天而不是幾周內(nèi)完全驗證接口。

可以通過編寫自定義屬性來驗證IP的特定塊，以驗證已實現(xiàn)的功能。可以使用新的選項，例如引入具有與UVM 記分板相同的眾所周知的概念的Formal 記分板，但是利用了Formal引擎的強大功能。它可用于驗證FIFO，通常用于處理數(shù)據(jù)路徑流但不是算術(shù)數(shù)據(jù)路徑的每個塊（例如加法器，乘法器）。

如今，主要的EDA公司制作了基于Formal流程的工具，這些工具使用時髦的技術(shù)詞匯：'APP'。這個概念是為“特定功能”的調(diào)試提供“隨時可用”的環(huán)境。這些APP自動生成斷言，并允許驗證工程師專注于調(diào)試RTL。

最有用的APP之一是用于驗證配置寄存器的訪問策略的APP。通過Formal流程，我們可以詳盡地驗證所有寄存器，尤其是最難驗證的狀態(tài)位，因為它們通常取決于HW狀態(tài)或特殊輸入條件。通常，流程基于IPXACT，然后也可以在設(shè)計開發(fā)的其他步驟中重復(fù)使用。此外，在這種情況下，這種驗證可以節(jié)省很多時間相對于'經(jīng)典'UVM隨機約束方法。

圖2：新數(shù)字IP的驗證流程

可用APP的數(shù)量正在快速增長，這將允許將驗證任務(wù)從動態(tài)移動到靜態(tài)，從而改善覆蓋范圍并縮短驗證時間。當(dāng)然，正式流程有一些局限性，目前無法用于驗證所有內(nèi)容;當(dāng)要分析的狀態(tài)數(shù)（即“形式復(fù)雜性指數(shù)”）太大時，引擎無法收斂并徹底分析代碼。這是一項挑戰(zhàn)，可以通過引入新算法和計算能力在不久的將來克服這一挑戰(zhàn)。無論如何，我們不能聲稱正式流程將超過動態(tài)模擬，原因很簡單：使用'假設(shè)'語句會引入隱藏錯誤的風(fēng)險，如果屬性成功，則有可能如果在實際應(yīng)用程序中未滿足假設(shè)條件，則RTL行為將是錯誤的。這完全類似于靜態(tài)時序分析（STA）和門級仿真：如果時序約束錯誤，STA表示設(shè)計中沒有時序違規(guī)，但最終設(shè)計不適用于某些極端情況。動態(tài)模擬允許我們驗證形式'假設(shè)'語句以及STA約束。

由于這些原因，驗證流程的下一步需要進(jìn)行UVM模擬，提升通過正式步驟中成功的屬性斷言，現(xiàn)在也可以在動態(tài)模擬中重復(fù)使用。在這個新流程中開發(fā)的測試數(shù)量將少于使用圖1所示流程開發(fā)的測試數(shù)量，因為我們可以專注于正式流程中發(fā)現(xiàn)的部分，并為使用它分析的部分開發(fā)有限的測試。

圖2所示流程的最后幾個步驟基本相同：我們運行不可達(dá)性分析以刪除無法訪問的代碼，然后分析代碼和功能覆蓋。

結(jié)論

使用形式驗證方法作為流程的第一步，代表了一種不同的方法，可以更好地利用正式的好處和有效性：零時間用于構(gòu)建測試平臺和RTL的詳盡驗證。此外，使用這種方法的學(xué)習(xí)曲線比UVM更快;用于編寫斷言的語言是緊湊的（PSL或SVA）并且易于使用。最困難的工作是用人類語言定義最能描述我們想要證明的功能的正確屬性。轉(zhuǎn)換為SVA或PSL變得簡單易行。

在RTL驗證的早期階段使用形式化方法的主要優(yōu)點是使用更清晰的代碼進(jìn)入動態(tài)模擬，其中許多功能已經(jīng)過徹底驗證并且修復(fù)了一些錯誤。由于正式方法允許我們縮短在驗證功能上花費的時間，因此可以大大縮短整體驗證時間。