1、SVA對時序及邏輯較為關心的模塊進行直接斷言檢查。以驗證DUT內部信號的時序關系是否符合預期

　　1、mem 接口：對1r1w的偽雙口ram，對2r2w的真雙口ram，的讀寫沖突進行檢測。

　　2、fsm狀態機：對狀態跳轉及狀態輸出進行監控。

　　3、coverage收集：某些場景下，信號的組合方式是否進行了測試，需要斷言進行cover。

2、SVA 語法及示例：

property?a2b_p;@(posedge?sclk)?$rose(a)?|->?[2:4]?$rose(b);? endproperty? a2b_a:?assert?property(a2b_p);? a2b_c:?cover?property(a2b_p);?

當信號a在某一個時鐘周期為高電平時，那么在接下來的2～4個時鐘周期內，信號b應該為高電平；

assert 檢測斷言是否滿足；

cover檢查該場景是否經過測試；

3、斷言分類：

　　1、即時斷言：

　　 ?即時斷言基于事件的變化，表達式的計算就像Verilog中的組合邏輯賦值一樣，是立即被求值的，而不是時序相關的。

always_combimmi_a:?assert?(a?&&?b);?

　　2、并發斷言：

　　并發斷言的計算基于時鐘周期，在時鐘邊沿根據變量的采樣值計算表達式。進行時序檢查時，通常使用并發斷言，而很少使用即時斷言。

　　

　　SVA提供了3個內嵌函數，用于檢查信號的邊沿變化。

　　

sequence?rose_s;@(posedge?sclk)?$rose(a); endsequence
sequence?fell_s;
　　@(posedge?sclk)?$fell(a); endsequencesequence?stable_s;@(posedge?sclk)?$stable(a); endsequence

上面的sequence會在每個sclk上升邊沿檢查斷言，雖然這些斷言是良性的，但它會在一段時間內產生大量的錯誤信息。

為了避免這種錯誤的產生，SVA提供了“蘊含”操作符（implication，|->）。其形式為：a?|->?b，

當先行算子匹配（成功）時，后序算子才能被計算。如果先行算子不成功，那么整個屬性就被默認成功，

蘊含操作符分為兩類：交疊蘊含操作符（overlapped?implication，|->）表示如果先行算子匹配，后序算子在同一個時鐘周期開始計算。

和非交疊蘊含操作符（non_overlapped?implication，|=>）如果先行算子匹配，后序算子在下一個時鐘周期開始計算。

序列的重復操作符分為3類：

連續重復：a[*3]”表示a被連續重復3次，“a[*1:3]”表示a被連續重復1～3次。連續重復的相鄰兩次重復之間只有一個時鐘間隔。

跳轉重復：a[->3]”表示a被跳轉重復3次，“a[->1:3]”表示a被跳轉重復1～3次。跳轉重復的相鄰兩次重復之間可以有任意時鐘間隔。

非連續重復：a[=3]”表示a被非連續重復3次，“a[=1:3]”表示a被非連續重復1～3次。非連續重復的相鄰兩次重復之間有任意多個時鐘間隔。最后一次也可以有任意時間間隔

?

?

轉載于:https://www.cnblogs.com/littleMa/p/5832111.html

與50位技術專家面對面20年技術見證，附贈技術全景圖

總結

以上是生活随笔為你收集整理的SVA的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。