一、序言

SVA，即SystemVerilog Assertion，在simulation和Formal都有極為廣泛的應用，這里介紹一些基本的概念和常用的語法。

二、一個簡單的例子

以一個arbiter仲裁器 作為例子來闡述一些概念，這個仲裁器有4個request來自不同的agent，req的每個bit表示相應的仲裁請求發起。gnt信號每個bit表示相應的請求被允許。同時，這里還有一個opcode輸入，用來override正常的請求，例如強制某個agent獲得grant，或者讓所有的gnt都無效一段時間。error信號表示一些錯誤的輸入序列或者錯誤的opcode。模塊框圖如下所示：

interface代碼如下：

三、基本概念

在介紹SVA之前，我們先來澄清幾個容易混淆的概念，尤其是assertion和assumption，傻傻分不清。

3.1 Assertion

assertion一般用來表示一個表達式恒為True，比如agent0未發起request，則gnt[0]不應該被拉起來。這種情形我們可以用assertion來加以檢查。

check_grant: assert property (!(gnt[0] && !req[0])) else $error(“Grant
without request for agent 0!”);

3.2 Assumption

assertion一般用于檢查DUT內部的狀態，而Assumption則主要用于約束驗證環境，主要用于約束輸入。例如我們期望opcode應該是合法的一些參數，就可以用assumption語句來進行約束。

good_opcode: assume property (opcode inside {FORCE0,FORCE1,FORCE2,
FORCE3,ACCESS_OFF,ACCESS_ON}) else $error(“Illegal opcode.”);

在simulation中，assumption跟assertion運行效果一樣，都是用來檢查輸入。但在Formal里面，二者則有很多的區別。對于上面那個assumption，在simulation中，不斷的檢測opcode，不在這些數里面則報一個assertion failure。在Formal里面，這是表示opcode激勵只能在這些數里面取值，大家可以將其理解成一個輸入的constraint。

3.3 COVER POINTS

這個沒什么好說的，在simulation和formal里面都是一致，用來表征覆蓋率。

不過需要注意的是，FV通常可以全覆蓋。但是因為有assumption，我們有時候會overconstraint ，這樣有些東西就可能被漏掉。所以coverpoint在FV里面至關重要。

一般來說，FV上來就先寫coverpoint，先規劃好哪些點需要覆蓋。其次還是assertion和assumption。這樣就不會出現過overconstraint而不自知的情形。

四、SVA 語法介紹

SVA Asssertion 語言分為幾個等級，自下而上，可以分成四個等級，即boolean、sequence、property和assertion statement，如下圖所示：

Booleans

Booleans 即布爾表達式，一些與或非的邏輯，例如:

(req[0]&&req[1]&&req[2]&&req[3])

Sequences

Sequences 顧名思義，就是boolean 表達式的序列，也就是說一段時間（幾個cycle）的booleans的組合，以來與clock event來定義這個區間，例如req0有效兩個cycle后gnt0有效

req[0] ##2 gnt[0]

Properties

Properties 則是進一步將sequences和一些操作符組合起來，表示一個implication或者其他的。比如：

req[0] ##2 gnt[0] |-> ##1 !gnt[0]

Assertion Statements

Assertion Statements 則是用assert, assume, cover等關鍵詞將properties例化，把SVA property 轉換成真正意義的assertion, assumption, cover point. 例如：

gnt_falls: assert property(req[0] ##2 gnt[0] |-> ##1 !gnt[0]);

另外還有兩個概念需要明確:

immediate assertions

Immediate assertion 簡單的assertion語句，只能用于procedural 語句里面。只支持booleans，不能有clock， reset或者property語句。

imm1: assert (!(gnt[0] && !req[0]))

concurrent assertions

Concurrent assertion 語句則一般用于檢查多個cycle期間段的一些property，一般我們說SVA基本代指Concurrent assertion

conc1: assert property (!(gnt[0] && !req[0]))

五、CONCURRENT 語法

concurrent assertion的一般寫法如下例所示:

safe_opcode: assert property (
@(posedge clk)
disable iff (rst)
(opcode inside {FORCE0,FORCE1,FORCE2,FORCE3,ACCESS_OFF,ACCESS_ON}))
else $error(“Illegal opcode.”);

一般包含下面幾點：

帶關鍵詞assert property.

帶clock

可選的disable iff語句

5.1 常用函數

SVA自帶了一些系統函數，這里列出一些常用的供參考。

5.2 Disable iff

Disable iff (iff表示if and only if)語句，顧名思義就是在某個條件成立的時候將assertion語句disable掉。但這里有點需要特別注意的是，diasable iff里面的邏輯采樣不是基于clock的，或者說相對clock來說是異步的。建議里面只放reset邏輯，不要放其他的邏輯。我們舉個例子，如果有gnt，那么鐵定有個req，兩種寫法：

bad_assert: assert property (@(posedge clk)
disable iff
(real_rst || ($countones(gnt) == 0))
($countones(req) > 0));

good_assert: assert property (@(posedge clk)
disable iff (real_rst)
(($countones(req) > 0) ||
($countones(gnt) == 0)));

表面上看，二者似乎一樣。仔細分析下，在clock 8的phase，由于gnt=0，整個assertion直接被disable，我們也就沒法檢測出上一個cycle的failure。

這里其實是涉及到SVA的采樣時間問題，或者說systemverilog的region問題，建議翻閱<> 這本書，里面有非常詳細的解讀。

六、SEQUENCE 語法

6.1 delay

sequence 基本的操作符是#,即delay，##n (延時特定個cycle) or ##[a:b] (延時 a 到b 個cycle) 。

6.2 repetition

repetition 操作符 [*m:n] ，表示subsequence 重復多少次。

6.3 logical ops

Sequences 可以通過and 或者or組合起來。

and: 兩個sequence同時start，但它們的結束點未必相同。

or: 兩個sequence至少有一個match

throughout : Boolean expression remains true for the whole execution of a sequence

within: one sequence occurs within the execution of another

6.4 go to repetetion

goto repetition 操作符，即 [- > n] 和 [ =n] ，表示有value重復了正好n次，未必是連續的cycle。

這兩個操作符如果后面不接其他的東西的話，是等價的。如果后面帶有其他的sequence的話，意義有點不一樣：

[->n]: goto repetition， 下一個sequence必須緊接著。

[=n]: nonconsecutive goto repetition， 下一個seuquece出現前允許插入若干個cycle的空閑

6.5 Implication

sequence |-> property ：sequence match后立即檢查property

sequence |=> property. ：sequence match后delay一個cycle再檢查property

左邊稱為antecedent （先決條件），必須為sequence；右邊稱為consequence （結果） ，可以是squence或者property。

需要強調一點，如果antecedent 在整個過程都不滿足的話，這個assertion也不會fail，這種情形在formal中稱為vacuously，即空的pass。

還有一些SVA語法，不是很常用，可以用到時候翻閱手冊查詢

六、MULTITHREADING

MULTITHREADING，即多線程。這里需要強調下，assertion的多線程屬性；每次antecedent為真，工具都將新啟動一個線程來check，我們以一個例子來進行說明。

req信號有效后，10個cycle之后gnt信號應該有效。代碼如下：

delayed_gnt: assert property (req[0] |->##10 gnt[0])

由于req和gnt之前隔了10個cycle，很有可能在這中間req信號再次被拉起，如果這樣的話，工具會啟多個線程，每個線程檢查相應的req和gnt對應的關系。

七、總結

SVA語法較多，需要反復練習才能掌握和精通。尤其是它的debug，需要反復實踐，加以體會。不建議寫很復雜的SVA，不方便debug。

審核編輯：劉清