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

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

通用驗(yàn)證流程

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

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

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

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

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

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

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

RTL錯(cuò)誤修復(fù)

功能和代碼覆蓋

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

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

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

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

新的驗(yàn)證流程

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

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

主要的變化是將形式驗(yàn)證作為流程的第一步。真正的第一個(gè)檢查是對(duì)死代碼和未初始化寄存器的分析。這是一項(xiàng)零工作任務(wù)，因?yàn)椴恍枰~外的代碼，并且它只需要使用Formal工具編譯RTL。隨后的反饋可能非常有用，因?yàn)樗梢宰屛覀儚氐浊謇鞷TL代碼，突出顯示從未到過的部分，以及列出可能導(dǎo)致'X'傳播的未初始化觸發(fā)器

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

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

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

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

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

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

由于這些原因，驗(yàn)證流程的下一步需要進(jìn)行UVM模擬，提升通過正式步驟中成功的屬性斷言，現(xiàn)在也可以在動(dòng)態(tài)模擬中重復(fù)使用。在這個(gè)新流程中開發(fā)的測(cè)試數(shù)量將少于使用圖1所示流程開發(fā)的測(cè)試數(shù)量，因?yàn)槲覀兛梢詫Ｗ⒂谡搅鞒讨邪l(fā)現(xiàn)的部分，并為使用它分析的部分開發(fā)有限的測(cè)試。

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

結(jié)論

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

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