眾所周知，在數字ip設計以及soc設計中，驗證任務迫在眉睫。目標是使rtl**和功能覆蓋率都達到100％，並最大程度地減少獲得它的時間。使用最廣泛的方法是基於通用驗證方法（universal verification methodology，uvm）的隨機約束測試（system verilog或e語言），它能夠在相對較短的時間內構造複雜的測試，同時強調rtl**並跟蹤功能覆蓋範圍。一些驗證工程師還使用形式化的方法來驗證模組的專用部分，例如標準介面，從而完成ip驗證。
本文將介紹一種基於形式方**來驗證數字ip的不同方法：通過定義屬性來詳盡地驗證功能。形式化方法的優點是避免開發測試平台。這種新流程已在數字ip的設計過程中使用，並已證明可大大縮短驗證時間。
通用驗證流程
當前，最常用的數字ip和片上系統（soc）驗證流程是基於uvm方法是使用驗證元件（verification components，vc）。該元件可以從第三方獲得，也可以在使用非標準協議時自行從頭開發。 然後，測試平台將完成包括用於自我資料檢查的記分板、用於驗證設計特定部分的斷言以及用於跟蹤功能覆蓋的覆蓋率。在過去的幾年中，形式驗證已開始在soc和ip的驗證流程中使用。在soc中，形式驗證在驗證soc外圍裝置和晶元管腳之間的連線性方面已變得非常普遍，主要是當多路復用方案是由連線到數量減少的晶元管腳和多個外圍裝置形成的，這增加了需要驗證的組合。有時，在ip驗證中，形式化方法用於檢查匯流排協議介面和暫存器訪問策略。
現在，我們聚焦於數字ip的驗證，可以將流程總結為圖1中所示的流程。當第一版rtl準備就緒時，好的驗證流程的第一步會始於定義驗證和測試計畫。在這個階段，我們將定義我們要檢查的功能和測試的框架。
下一步是開發uvm測試平台；搭建定製的uvm塊用於檢查特定的ip功能，同時第三方的uvm vc則被例項化並繫結到rtl。
此時，我們可以根據驗證計畫開發uvm測試用例。每個驗證工程師都需要記住的第一件事是測試必須是自動檢測的。驗證計畫中列出的所有點都必須使用記分板、檢查器和斷言來自動檢查。然後，覆蓋結構的廣泛使用可以量化測試的質量。
圖1：數字ip的通用驗證流程
有時，該流程可能包括形式驗證。在驗證任務的某個時刻，有人可能會決定使用基於斷言的驗證ip（assertion-based verification ip，abvip）來檢查ip的特定塊（例如匯流排協議介面）,以及通過編寫斷言來檢查通過有限狀態機（fsm）實現的精確功能。
眾所周知，驗證任務是乙個具有兩個主要環迴的迭代過程：
每當我們發現功能規範與ip行為之間不匹配時，就會將其作為可能的錯誤告知設計人員。這意味著需要修改rtl並發布新的固定版本。現在，關鍵是要進行回歸式自我檢查測試（即使最初是部分測試），這使我們能夠驗證rtl**有沒有回歸，當然，就是看該錯誤是否已得到修復。此環回也可以來自形式驗證。
開發出足夠數量的測試後，好的作法是對功能和**覆蓋率進行度量。通常，功能和**覆蓋率的目標都是100％，但是我們必須考慮為此所花費的時間。如果我們希望在確保目標為100％的前提下最小化時間，則必須改進驗證的方法和流程。來自形式化世界的乙個很好的建議是**不可達性分析，它有助於發現rtl不可訪問的部分，可以從整個**覆蓋範圍中刪除這些部分。
一條很好的經驗法則：「如果我不練習**的一部分，那麼很可能會出現錯誤。」因此，我們花了很多時間來觸發未覆蓋的**，但是知道這部分**無法到達將節省我們的時間和精力。
接下來，我們將描述乙個新流程，其主要目標是減少數字ip驗證所花費的時間，同時保持覆蓋率的目標。
新的驗證流程
形式化方法是一種詳盡的驗證，並且在適用時，它使人們可以在更短的時間內針對模組功能的每種可能情況進行檢查。對於普通的動態**，有時這是不可行的。
當前，有幾種工具可以鏈結到形式化引擎，這些工具已經足夠成熟，可以使圖1所示的驗證流程變為圖2所示的內容。
主要變化是將形式驗證引入流程作為第一步。真正的第一步檢查是分析死**和未初始化的暫存器。這是一項沒有額外負擔的任務，因為不需要額外的**，並且只需要使用形式工具來編譯rtl。隨後的反饋可能非常有用，因為它使我們能夠對rtl**進行徹底的清理，突出顯示從未達到的部分，並列出可能導致「 x」傳播的未初始化觸發器的列表。
毫無疑問，可以使用專用的基於斷言的vip（abvip）在短時間內完全驗證諸如微處理器匯流排介面之類的標準協議。形式化流程的這些驗證元件是基於描述協議的斷言。驗證工程師將專注於除錯失敗的屬性，而無需花費時間在測試台和屬性開發上。通過用形式化驗證替代uvm流，我們可以在幾天（而不是幾周）內對介面進行完全驗證。
ip的特定模組可以通過編寫自定義屬性用以驗證已實現的功能。新的可用選項包含，例如引入形式記分板，該記分板具有與uvm記分板相同的概念，但是利用了形式化引擎的功能。它可用於fifo的驗證，並且通常來說，該方法適用於每個在資料流上但不包含算術資料路徑（例如加法器，乘法器）的模組。
圖2：數字ip的全新驗證流程
由於這些原因，驗證流程的下一步需要的是uvm**，這是增強通過形式化步驟中成功的屬性宣告，現在也可以在動態**中重新使用。在這個新流程中開發的測試數量將少於使用圖1中所示的流程開發的測試數量，因為我們可以專注於形式化流程未覆蓋的部分，並為分析這些部件開發有限的測試。
圖2中顯示的流程的最後一步基本相同：我們進行不可達性分析以刪除不可達**，然後分析**和功能覆蓋率。
結論使用形式化驗證方法作為流程的第一步，代表了一種不同的方法，可以更好地利用形式化的好處和有效性：無需耗時用於構建測試平台和rtl的詳盡驗證。而且，使用這種方法的學習曲線比uvm更快。用於編寫斷言的語言很緊湊（psl或sva）並且易於使用。最困難的工作是用人工語言定義正確的屬性，以最好地描述我們要證明的功能。轉換為sva或psl變得相對容易。
在rtl驗證的早期階段使用形式化方法的主要優點是可以使用更清晰的**進入動態**，其中許多功能已經得到詳盡的驗證，並且修復了一些錯誤。由於形式化方法允許我們減少花在功能驗證上的時間，因此可以大大減少整體驗證時間。
我們使用此新流程進行ip驗證（具有用於配置和資料交換的amba介面），並且在驗證rtl**上所花費的時間減少了30％以上。
可直達課程頁面，馬上試聽
往期精彩：
路科發布| 穩中帶漲！25w成晶元校招薪資平均底！2020應屆秋招資料全面分析！
相約今晚8點 社招轉崗有顧慮？成功上岸的同學來幫你
v2pro 2020秋m1 我對你的迷惑和選擇都深以為然
v2pro春季班普遍學撐了，秋季班7月報名你還敢來麼
uvm ral模型：用法和應用
我們準備做第二期線下培訓，依舊認真且嚴肅
如果你突然被裁員了，你的plan b是什麼？
[彩虹糖帶你入門uvm]
理解uvm-1.2到ieee1800.2的變化，掌握這3點就夠
OS形式化設計與驗證
os往往無法提供理想的安全服務和安全保障。這主要存在兩方面的原因,首先在os實現過程中os開發者不可避免地存在程式設計錯誤 實現與設計不一致等問題,另外更重要的是在os設計過程存在os功能設計與安全目標不一致等問題。目前,公認的 最為合理的方案是利用嚴格的形式化方法來對os進行設計實現和驗證。形式化...
IC設計崗位之數字前端設計 驗證 後端要怎麼選擇？
ic設計崗位選擇上的建議 對於design設計而言，他可能對於理論知識，比如說像演算法協議，他的前沿性可能更強一點，可能要求會相對高一點，看你那方面更擅長。驗證工程師的coding能力就於今天的崗位而言，他的coding能力可能要求更高一點。為什麼？因為很多東西這麼多年的積累，我們把很多驗證的模組都...
IC設計職位詳解之「數字驗證工程師」就業必學課程
數字驗證處於數字ic設計流程的前端，屬於數字ic設計類崗位的一種。在ic設計中，數字驗證所佔的人數比重是非常多的，很多大公司，數字前端設計工程師與驗證工程師的比例已經達到1 3。數字驗證主要分成幾種層次的驗證 ip level，unitlevel，fullchip soc level，gatelev...