一、序言

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

二、一個(gè)簡(jiǎn)單的例子

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

interface代碼如下：

三、基本概念

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

3.1 Assertion

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

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語(yǔ)句來(lái)進(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)行效果一樣，都是用來(lái)檢查輸入。但在Formal里面，二者則有很多的區(qū)別。對(duì)于上面那個(gè)assumption，在simulation中，不斷的檢測(cè)opcode，不在這些數(shù)里面則報(bào)一個(gè)assertion failure。在Formal里面，這是表示opcode激勵(lì)只能在這些數(shù)里面取值，大家可以將其理解成一個(gè)輸入的constraint。

3.3 COVER POINTS

這個(gè)沒(méi)什么好說(shuō)的，在simulation和formal里面都是一致，用來(lái)表征覆蓋率。

不過(guò)需要注意的是，F(xiàn)V通常可以全覆蓋。但是因?yàn)橛衋ssumption，我們有時(shí)候會(huì)overconstraint ，這樣有些東西就可能被漏掉。所以coverpoint在FV里面至關(guān)重要。

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

四、SVA 語(yǔ)法介紹

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

Booleans

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

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

Sequences

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

req[0] ##2 gnt[0]

Properties

Properties 則是進(jìn)一步將sequences和一些操作符組合起來(lái)，表示一個(gè)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]);

另外還有兩個(gè)概念需要明確:

immediate assertions

Immediate assertion 簡(jiǎn)單的assertion語(yǔ)句，只能用于procedural 語(yǔ)句里面。只支持booleans，不能有clock， reset或者property語(yǔ)句。

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

concurrent assertions

Concurrent assertion 語(yǔ)句則一般用于檢查多個(gè)cycle期間段的一些property，一般我們說(shuō)SVA基本代指Concurrent assertion

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

五、CONCURRENT 語(yǔ)法

concurrent assertion的一般寫(xiě)法如下例所示:

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語(yǔ)句

5.1 常用函數(shù)

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

5.2 Disable iff

Disable iff (iff表示if and only if)語(yǔ)句，顧名思義就是在某個(gè)條件成立的時(shí)候?qū)ssertion語(yǔ)句disable掉。但這里有點(diǎn)需要特別注意的是，diasable iff里面的邏輯采樣不是基于clock的，或者說(shuō)相對(duì)clock來(lái)說(shuō)是異步的。建議里面只放reset邏輯，不要放其他的邏輯。我們舉個(gè)例子，如果有g(shù)nt，那么鐵定有個(gè)req，兩種寫(xiě)法：

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，整個(gè)assertion直接被disable，我們也就沒(méi)法檢測(cè)出上一個(gè)cycle的failure。

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

六、SEQUENCE 語(yǔ)法

6.1 delay

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

6.2 repetition

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

6.3 logical ops

Sequences 可以通過(guò)and 或者or組合起來(lái)。

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

or: 兩個(gè)sequence至少有一個(gè)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。

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

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

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

6.5 Implication

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

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

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

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

還有一些SVA語(yǔ)法，不是很常用，可以用到時(shí)候翻閱手冊(cè)查詢

六、MULTITHREADING

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

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

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

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

七、總結(jié)

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

審核編輯：劉清