systemverilog_斷言_快速教程

1、Bind: very useful in systemverilog.Assertion: 1# “a #3 b”意思是a 之后3個(gè)周期b. 2“|-”表示如果先行算子匹配，后序算子在同一周期開始計(jì)算3“|=” 表示如果先行算子匹配，后序算子在下一個(gè)周期開始計(jì)算4重復(fù)操作符：*連續(xù)重復(fù) “*m”: “a*1:3” 表示a被連續(xù)重復(fù)13次*跳轉(zhuǎn)重復(fù) “-”: “a-3” 表示a被跳轉(zhuǎn)重復(fù)3次*非連續(xù)重復(fù) “=m”: “a=3” 表示a被非連續(xù)重復(fù)3次芯片設(shè)計(jì)：verilog斷言（SVA）語(yǔ)法斷言assertion被放在verilog設(shè)計(jì)中，方便在仿真時(shí)查看異常情況。當(dāng)異常出現(xiàn)時(shí)，斷言會(huì)報(bào)警。一般

2、在數(shù)字電路設(shè)計(jì)中都要加入斷言，斷言占整個(gè)設(shè)計(jì)的比例應(yīng)不少于30%。以下是斷言的語(yǔ)法：1. SVA的插入位置：在一個(gè).v文件中：module ABC ();rtl 代碼SVA斷言endmodule注意：不要將SVA寫在enmodule外面。2. 斷言編寫的一般格式是：【例】 斷言名稱1：assert property(事件1) /沒有分號(hào)$display(.,$time); /有分號(hào)else$display(.,$time); /有分號(hào)斷言名稱2：assert property(事件2)$display(.,$time);else$display(.,$time);斷言的目的是：斷定“事件1”和

3、“事件2”會(huì)發(fā)生，如果發(fā)生了，就記錄為pass，如果沒發(fā)生，就記錄為fail。注意：上例中沒有if，只有else，斷言本身就充當(dāng)if的作用。上例中，事件1和事件2可以用兩種方式來寫：(1) 序列塊：sequence name;。;endsequence(2) 屬性塊： property name;。;endsequence從定義來講，sequence塊用于定義一個(gè)事件（磚），而property塊用于將事件組織起來，形成更復(fù)雜的一個(gè)過程（樓）。sequence塊的內(nèi)容不能為空，你寫亂字符都行，但不能什么都沒有。sequence也可以包含另一個(gè)sequence, 如：sequence s1;s2(

4、a,b);endsequence /s1和s2都是sequence塊sequence塊和property塊都有name，使用assert調(diào)用時(shí)都是：“assert property(name);”在SVA中，sequence塊一般用來定義組合邏輯斷言，而property一般用來定義一個(gè)有時(shí)間觀念的斷言，它會(huì)常常調(diào)用sequence，一些時(shí)序操作如“|-”只能用于property就是這個(gè)原因。注：以下介紹的SVA語(yǔ)法，既可以寫在sequence中，也可以寫在property中，語(yǔ)法是通用的。3. 帶參數(shù)的property、帶參數(shù)的sequenceproperty也可以帶參數(shù)，參數(shù)可以是事件或信號(hào)

5、，調(diào)用時(shí)寫成：assert property (p1(a,b)被主sequence調(diào)用的從sequence也能帶參數(shù)，例如從sequence名字叫s2，主sequence名字叫s1:sequence s1;s2(a,b);endsequence4. property內(nèi)部可以定義局部變量，像正常的程序一樣。property p1;int cnt;.endproperty【注】在介紹語(yǔ)法之前，先強(qiáng)調(diào)寫斷言的一般格式：一般，斷言是基于時(shí)序邏輯的，單純進(jìn)行組合邏輯的斷言很少見，因?yàn)樘M(fèi)內(nèi)存（時(shí)序邏輯是每個(gè)時(shí)鐘周期判斷一次，而組合邏輯卻是每個(gè)時(shí)鐘周期內(nèi)判斷多次，內(nèi)存吃不消）。因此，寫斷言的一般規(guī)則是：

6、time + event，要斷定發(fā)生什么event，首先要指定發(fā)生event的時(shí)間，例如每個(gè)時(shí)鐘上升沿 + 發(fā)生某事某信號(hào)下降時(shí) + 發(fā)生某事5. 語(yǔ)法1：信號(hào)（或事件）間的“組合邏輯”關(guān)系：(1) 常見的有：&, |, !, (2) a和b哪個(gè)成立都行，但如果都成立，就認(rèn)為是a成立：firstmatch(a|b)，與“|”基本相同，不同點(diǎn)是當(dāng)a和b都成立時(shí)，認(rèn)為a成立。(3) a ? b:c a事件成功后，觸發(fā)b，a不成功則觸發(fā)c6. 語(yǔ)法2：在“時(shí)序邏輯”中判斷獨(dú)立的一根信號(hào)的行為： (posedge clk) A事件; 當(dāng)clk上升沿時(shí)，如果發(fā)生A事件，斷言將報(bào)警。邊沿觸發(fā)內(nèi)置函數(shù)：(假

7、設(shè)存在一個(gè)信號(hào)a)$rose( a ); 信號(hào)上升$fell( a ); 信號(hào)下降$stable( a ); 信號(hào)值不變7. 語(yǔ)法3：在“時(shí)序邏輯”中判斷多個(gè)事件/信號(hào)的行為關(guān)系：(1) intersect(a,b) 斷定a和b兩個(gè)事件同時(shí)產(chǎn)生，且同時(shí)結(jié)束。(2) a within b 斷定b事件發(fā)生的時(shí)間段里包含a事件發(fā)生的時(shí)間段。(3) a #2 b 斷定a事件發(fā)生后2個(gè)單位時(shí)間內(nèi)b事件一定會(huì)發(fā)生。a #1:3 b 斷定a事件發(fā)生后13個(gè)單位時(shí)間內(nèi)b事件一定會(huì)發(fā)生。a #3:$ b 斷定a事件發(fā)生后3個(gè)周期時(shí)間后b事件一定會(huì)發(fā)生。(4) c throughout (a #2 b) 斷定在a

8、事件成立到b事件成立的過程中，c事件“一直”成立。(5) (posedge clk) a |- b 斷定clk上升沿后，a事件“開始發(fā)生”，同時(shí)，b事件發(fā)生。(6) (posedge clk) a.end |- b 斷定clk上升沿后，a事件執(zhí)行了一段時(shí)間“結(jié)束”后，同時(shí)，b事件發(fā)生。注：a |- b 在邏輯上是一個(gè)判斷句式，即：if ab;elsesucceed;因此，一旦 a 發(fā)生，b 必須發(fā)生，斷言才成功。如果a沒發(fā)生，走else，同樣成功。 (7) (posedge clk) a |= b 斷定clk上升沿后，a事件開始發(fā)生，下一個(gè)時(shí)鐘沿后，b事件開始發(fā)生。(8) (posedge c

9、lk) a |=#2b 斷定clk上升沿后，a事件開始發(fā)生，下三個(gè)時(shí)鐘沿后，b事件開始發(fā)生。(9) (posedge clk)$past(a,2) = 1b1 斷定a信號(hào)在2個(gè)時(shí)鐘周期“以前”，其電平值是1。(10) (posedge clk) a *3 斷定“ (posedge clk) a”在連續(xù)3個(gè)時(shí)鐘周期內(nèi)都成立。 (posedge clk) a *1:3 斷定“ (posedge clk) a”在連續(xù)13個(gè)時(shí)鐘周期內(nèi)都成立。 (posedge clk) a -3 斷定“ (posedge clk) a”在非連續(xù)的3個(gè)時(shí)鐘周期內(nèi)都成立。舉一個(gè)復(fù)雜點(diǎn)的例子：property ABC;in

10、t tmp;(posedge clk) ($rose(a),tmp = b) |- #4 (c = (tmp*tmp+1) #3 d*3;endproperty上例的一個(gè)property說明：當(dāng)clk上升沿時(shí)，斷言開始。首先斷定信號(hào)a由低變高，將此時(shí)的信號(hào)b的值賦給變量tmp，4個(gè)時(shí)鐘周期后，斷定信號(hào)c的值是4個(gè)周期前b2+1，再過3個(gè)周期，斷定信號(hào)d一定會(huì)起來，再過3個(gè)周期，信號(hào)d又起來一次。只有這些斷定都成功，該句斷言成功。otherwise，信號(hào)a從一開始就沒起來，則斷言也成功。8. 語(yǔ)法4：多時(shí)鐘域聯(lián)合斷言：一句斷言可以表示多個(gè)時(shí)鐘域的信號(hào)關(guān)系，例如： （posedge clk1） a

11、 |- #1 (posedge clk2) b當(dāng)clk1上升沿時(shí)，事件a發(fā)生，緊接著如果過來第二個(gè)時(shí)鐘clk2的上升沿，則b發(fā)生?！?1”在跨時(shí)鐘時(shí)不表示一個(gè)時(shí)鐘周期，只表示等待最近的一個(gè)跨時(shí)鐘事件。所以此處不能寫成#2或其他。但是可以寫成： （posedge clk1） a |= (posedge clk2) b9. 語(yǔ)法5：總線的斷言函數(shù)總線就是好多根bit線，共同表示一個(gè)數(shù)。SVA提供了多bit狀態(tài)一起判斷的函數(shù)，即總線斷言函數(shù)：(1) $onehot(BUS) BUS中有且僅有1 bit是高，其他是低。(2) $onehot0(BUS) BUS中有不超過1 bit是高，也允許全0。(3

12、) $isunknown(BUS) BUS中存在高阻態(tài)或未知態(tài)。(4) countones(BUS)=n BUS中有且僅有n bits是高，其他是低。10. 語(yǔ)法6：屏蔽不定態(tài)當(dāng)信號(hào)被斷言時(shí)，如果信號(hào)是未復(fù)位的不定態(tài)，不管怎么斷言，都會(huì)報(bào)告：“斷言失敗”，為了在不定態(tài)不報(bào)告問題，在斷言時(shí)可以屏蔽。如： (posedge clk) (q = $past(d)，當(dāng)未復(fù)位時(shí)報(bào)錯(cuò)，屏蔽方法是將該句改寫為：(posedge clk) disable iff (!rst_n) (q = $past(d) /rst是低電平有效10. 語(yǔ)法6：斷言覆蓋率檢測(cè)：name: cover property (fun

13、c_name)11. 在modelsim中開啟斷言編譯和顯示功能：（1）【編譯verilog代碼時(shí)按照system verilog進(jìn)行編譯】 vlog -sv abc.v（2）【仿真命令加一個(gè)-assertdebug】 vsim -assertdebug -novopt testbench（3）【如果想看斷言成功與否的分析，使用打開斷言窗口的命令】 view assertions12. 在VCS中加入斷言編譯和顯示功能：在fsdb文件中加一句話：$fsdbDumpSVA在VCS編譯參數(shù)：system vcs $VCS_SIMULATION 中加入一些options:-assert enable

14、_diag-assert vpiSeqBeginTime-assert vpiSeqFail-assert report=路徑-assert finish_maxfail=100*【經(jīng)驗(yàn)】以下是一些編寫斷言的經(jīng)驗(yàn)：1. 斷言的目的：傳統(tǒng)的驗(yàn)證方法是通過加激勵(lì)，觀察輸出。這種方法對(duì)案例的依賴嚴(yán)重，案例設(shè)計(jì)不好，問題不便于暴露。而斷言是伴隨RTL代碼的，不依賴測(cè)試案例，而是相對(duì)“靜態(tài)”。例如：我們要測(cè)試一個(gè)串行數(shù)據(jù)讀寫單元，數(shù)據(jù)線只有一根，先傳四位地址，再傳數(shù)據(jù)。（1）案例驗(yàn)證法：寫一個(gè)地址，再寫一段數(shù)據(jù)，然后讀取該地址，看輸出的是不是剛才寫的數(shù)據(jù)。（2）斷言法：不需要專門設(shè)計(jì)地址和數(shù)據(jù)，當(dāng)發(fā)起寫

15、時(shí)，在地址傳輸?shù)臅r(shí)間里將地址存儲(chǔ)到一個(gè)變量里，在數(shù)據(jù)傳輸?shù)臅r(shí)間里將數(shù)據(jù)存儲(chǔ)到一個(gè)變量里，觀察RAM中該地址是否存在該數(shù)據(jù)就可以了。斷言設(shè)計(jì)相當(dāng)于在電腦上把RTL實(shí)現(xiàn)的功能再實(shí)現(xiàn)一遍。2. 斷言中可以包含function和task。而且function經(jīng)常用于斷言，因?yàn)橛械奶幚砗軓?fù)雜，而斷言又是“一句式”的，無法分成好幾句進(jìn)行表達(dá)，所以需要function替斷言分擔(dān)工作。3. 斷言允許規(guī)定同時(shí)發(fā)生的事件，就是組合邏輯，你可以寫成：a & b，也可以寫成 a #0 b，不能寫 #0.5，不支持小數(shù)。4. 斷言是用電腦模仿RTL的運(yùn)行過程，當(dāng)RTL功能復(fù)雜時(shí)，你必須用到變量。斷言中支持C語(yǔ)言的int

16、和數(shù)組聲明，但在賦值時(shí)“不能”寫成：#4 var = Signal，其中var是斷言中的變量，和RTL無關(guān)，Signal是RTL中的一個(gè)信號(hào)。本句是想在第4周期將Signal的值賦給var，以便在后面使用該值。但本句只有變量賦值，沒有對(duì)RTL信號(hào)的任何斷言，就會(huì)報(bào)錯(cuò)，解決方法是：#4 (“廢話”，var = Signal)，一定要有斷言的話我們就寫“廢話”，例如:data = data 等。如果有多個(gè)變量要賦值也可以，#4 （廢話，變量1賦值，變量2賦值.）5. 關(guān)于斷言的表達(dá)風(fēng)格：語(yǔ)法介紹的 “a |- b”，實(shí)際上是 “if a, then b”的邏輯，當(dāng)a不發(fā)生，b也不會(huì)被判斷，該斷言自

17、然成功。但當(dāng)我們的邏輯是if a1if a2then b該如何用斷言表達(dá)？ 或許可以寫成：“a1 |- a2 |- b”，也可以，但常用的表達(dá)是：“a1 & a2 |- b” 或者 “a1 #3 a2 |- b”6. 關(guān)于斷言的時(shí)序：時(shí)序邏輯的斷言需要注意的一個(gè)問題：例如：假設(shè)當(dāng)clk上升沿到來時(shí)，b=a。將上述邏輯寫成斷言時(shí)，如果寫成“(posedge clk) b=a”，看起來和 b=a一樣，但實(shí)際上是錯(cuò)的。因?yàn)楫?dāng)時(shí)鐘上升時(shí)，b還沒有得到a的值，a還需要一段保持時(shí)間。即，斷言中的信號(hào)值實(shí)際上是時(shí)鐘沿到來之前的值，而不是時(shí)鐘沿到來后他們將要編程的值。所以，b (b=tmp);”針對(duì)上述幾點(diǎn)，

18、舉一個(gè)復(fù)雜的例子：斷言wr的功能是檢查串行地址輸入是否正確，串行地址輸入線是DataIn 。$time返回值以0.1ns為單位（因?yàn)槲以趖estbench中的單位規(guī)定是timescale 1ns/100ps，精度是100ps = 0.1ns），所以$time/10才是ns。/wr: assert property(wr_p)$display(succeed：,$time/10);else$display(error: ,$time/10);/斷言可以聲明一個(gè)int數(shù)組arr4，/“(posedge clk) !vld_pulse_r0 & !DataIn”是真實(shí)的預(yù)備條件/“#4 (read=read, arr0 = DataIn)”只是為了在特定時(shí)間內(nèi)賦值，有用