一、序言

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

二、一個簡單的例子

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

interface代碼如下：

三、基本概念

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

3.1 Assertion

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

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

3.2 Assumption

assertion一般用于檢查DUT內(nèi)部的狀態(tài)，而Assumption則主要用于約束驗(yàn)證環(huán)境，主要用于約束輸入。例如我們期望opcode應(yīng)該是合法的一些參數(shù)，就可以用assumption語句來進(jìn)行約束。

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

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

3.3 COVER POINTS

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

不過需要注意的是，F(xiàn)V通?？梢匀采w。但是因?yàn)橛衋ssumption，我們有時候會overconstraint ，這樣有些東西就可能被漏掉。所以coverpoint在FV里面至關(guān)重要。

一般來說，F(xiàn)V上來就先寫coverpoint，先規(guī)劃好哪些點(diǎn)需要覆蓋。其次還是assertion和assumption。這樣就不會出現(xiàn)過overconstraint而不自知的情形。

四、SVA 語法介紹

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

Booleans

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

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

Sequences

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

req[0] ##2 gnt[0]

Properties

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

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

Assertion Statements

Assertion Statements 則是用assert, assume, cover等關(guān)鍵詞將properties例化，把SVA property 轉(zhuǎn)換成真正意義的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.”);

一般包含下面幾點(diǎn)：

帶關(guān)鍵詞assert property.

帶clock

可選的disable iff語句

5.1 常用函數(shù)

SVA自帶了一些系統(tǒng)函數(shù)，這里列出一些常用的供參考。

5.2 Disable iff

Disable iff (iff表示if and only if)語句，顧名思義就是在某個條件成立的時候?qū)ssertion語句disable掉。但這里有點(diǎn)需要特別注意的是，diasable iff里面的邏輯采樣不是基于clock的，或者說相對clock來說是異步的。建議里面只放reset邏輯，不要放其他的邏輯。我們舉個例子，如果有g(shù)nt，那么鐵定有個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)));

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

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

六、SEQUENCE 語法

6.1 delay

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

6.2 repetition

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

6.3 logical ops

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

and: 兩個sequence同時start，但它們的結(jié)束點(diǎn)未必相同。

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重復(fù)了正好n次，未必是連續(xù)的cycle。

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

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

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

6.5 Implication

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

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

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

需要強(qiáng)調(diào)一點(diǎn)，如果antecedent 在整個過程都不滿足的話，這個assertion也不會fail，這種情形在formal中稱為vacuously，即空的pass。

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

六、MULTITHREADING

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

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

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

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

七、總結(jié)

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

審核編輯：劉清