SV 使用斷言(Assertion)的優點

2021-10-06 09:25:58 字數 2109 閱讀 2933

朋友們,這次我決定寫關於斷言的文章。我個人認為斷言是非常方便和非常有用的資產,當我們談**能驗證時,即在給定的rtl設計中發現缺陷;確保驗證完整性。它是一種令人驚嘆的驗證技術,用較少的**提供了如此多的好處。如果你閱讀了我之前關於斷言的文章《關於斷言的基礎知識》,我們在這裡討論了乙個斷言示例,並與相應的verilog**進行了比較。在這裡,讓我們討論將斷言作為驗證過程的一部分的其他許多優點。

在乙個典型的設計中,我們有狀態元素,如flops, combo logic, fifo(先進先出),fsm(有限狀態機),計數器等。如果我們假設這個設計包含典型設計通常具有的rtl缺陷,那麼我們對主要輸入應用刺激,並觀察主要輸出的響應。假設測試失敗,我們通常會怎麼做?我們開始除錯意味著從主要輸出開始進行回溯跟蹤。我們需要繼續深入設計,直到找到失敗的根本原因。最後,我們解決了問題,但要找到問題的根源需要很長時間。這種方法通常被稱為黑盒測試,但重要的是,可觀察性在這種方法中也是黑盒測試。

現在讓我們假設,我們在設計中圍繞不同的邏輯元素插入斷言,並且在模擬期間斷言失敗。通過斷言,可以直接在源**中觀察到內部錯誤的根本原因。**時間。因此,插入斷言之後,我們可以說我們現在正在使用白盒可觀察性進行黑盒測試。這裡的底線是斷言可以幫助改進設計內部的可觀察性,從而縮短除錯時間。

在我們的設計中,我們想要確保所有的空間和時間條件都被提供的刺激所覆蓋或運用,並且事物都按照設計的規範執行。斷言覆蓋特性有助於提供關於各種設計元素(如fifo、fsms、計數器)的報告或覆蓋狀態。此外,對於主要輸入、主要輸出和模組間通訊的臨時行為需求,cover也非常有用。

讓我們假設我們為fifo full條件編寫了乙個斷言,但是對於當前的一組刺激,這個斷言永遠不會觸發。我們可以假設一切正常,因為在模擬日誌檔案中沒有斷言失敗。但是,如果所提供的刺激從未觸發fifo full條件,情況又會如何呢?在這種情況下,分析斷言覆蓋特性生成的報告將向我們展示給定刺激所覆蓋的內容和未覆蓋的內容。它肯定會幫助我們縮短時間,以涵蓋設計的所有預期場景。

現在,我們幾乎找不到單時鐘的設計,大多數今天的設計是基於多時鐘域的。當跨越不同的時鐘域時,使用多個時鐘斷言屬性對於資料完整性檢查非常有幫助。

如果在開發斷言時考慮到意圖,那麼斷言可以在多個專案中重用。眾所周知,可重用性是節省時間和精力的乙個重要因素。為未來專案而努力。可以通過以下兩種方式編寫斷言,以提高斷言的可重用性:

第一種方法是盡可能地實現引數化斷言。如果使用引數化,現在為16位匯流排編寫的斷言可以在將來的設計中為32位匯流排重用。

第二種方法是在rtl設計之外實現斷言模型,並將其作為單獨的實體進行維護。可以很容易地將這些斷言(使用bind特性)繫結到rtl,使設計和斷言**保持分離。它易於維護,最重要的是,如果使用適當的指導方針進行編碼,它是可重用的。

這意味著除非我們關閉斷言,否則斷言總是活動的。我們在測試套件中新增的測試用例或建立的新刺激配置越多,活動斷言就總是能夠監視針對新刺激的設計行為。

由於斷言合成現在已經成熟,這意味著斷言在模擬期間非常有用。由於我們知道dut被放置在**盒內的矽上,因此相關的斷言也可以隨著設計一起放置在**盒內。有了這種支援,在模擬執行中,與模擬相比執行得非常快,通常需要大量時間的除錯可以更快地完成。

斷言支援全域性嚴重性級別,例如$error、$fatal、$warning等。因此,它有助於在模擬中維護統一的錯誤報告機制或結構。

斷言支援全域性開啟/關閉機制,例如$dumpon/$dumpoff。它有助於以一種更簡單的方式維護**,而不是用開/關條件包裝每個斷言。

現在,天靜態形式驗證日益流行。斷言是關鍵元素,它定義了作為正式驗證技術一部分的設計的假設和預期行為。

靜態形式驗證不需要像在**中那樣在設計的主要輸入端應用任何動態向量,但是eda工具的內部演算法生成內部流量來檢查包含的斷言。確保設計的正確性。由於形式驗證是對從邏輯錐中匯出的代數方程進行的,因此邏輯錐中可能有許多輸入,這些輸入可能具有已知值,例如1或0。這些已知的值是使用斷言assume特性分配的,這樣,正式的工具執行輸入時的排列和組合就會更少,並通過有意義的努力產生建設性的結果。

斷言又稱為sva (systemverilog斷言)是這樣一種語言,它以多種方式為設計的驗證方面做出貢獻。斷言斷言功能通過設計檢查和形式化驗證(沒有動態向量的技術)工作,斷言覆蓋功能支援功能性覆蓋檢查,並假設功能滿足用於形式化驗證的設計約束。

它清楚地表明,sva是一種語言,它在支援約束隨機驗證(crv)、靜態形式驗證(sfv)和**/加速方面具有許多方面和優點。

斷言(assertion)的簡介

最常用的斷言定義方法是開放驗證庫ovl提供的宣稱性斷言。ovl是基於verilog的開放原始碼的斷言監督元件庫,以相同方式在rtl中定義靜態和動態斷言 提供統一的訊息報告機制 易於定製 提供一致安全級別,發生嚴重錯誤時可停止模擬。由於原始碼開放,能夠根據應用進行定製,因此ovl很吸引人。ovl使用斷...

SV斷言在測試激勵中的應用

本文 在我們平常的驗證過程中,有這樣的一種問題存在 乙個測試激勵根本沒有測試到我們期望的測試點,但是在 的過程中也沒有出現嚴重的錯誤,從頭到尾 正常的結束,那麼我們一般會認為它 通過了,在我們收集覆蓋率之前我們一般不會發現它其實根本什麼都沒有做,只是假裝 通過,今天我們介紹一種克服這種問題的辦法,利...

SV 中巨集的使用

在sv中,養成使用巨集的習慣可以大大提高code 的可閱讀性,讓我們從簡單重複的工作中脫離出來,聚焦技術方法本身或者硬體的理解上,可以有效的提高我們的驗證效率。在我們驗證的過程或多或少的會遇到在tb test中使用巨集的方法,當然我們是看的懂的,但是我們一定要思考這個tb test為什麼要這麼寫,有...