作者：白櫟旸
斷言assertion被放在verilog設(shè)計(jì)中，方便在仿真時(shí)查看異常情況。當(dāng)異常出現(xiàn)時(shí)，斷言會(huì)報(bào)警。一般在數(shù)字電路設(shè)計(jì)中都要加入斷言，斷言占整個(gè)設(shè)計(jì)的比例應(yīng)不少于30%。以下是斷言的語法：
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”和“事件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(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語法，既可以寫在sequence中，也可以寫在property中，語法是通用的。
3. 帶參數(shù)的property、帶參數(shù)的sequence
property也可以帶參數(shù)，參數(shù)可以是事件或信號(hào)，調(diào)用時(shí)寫成：assert property (p1(a,b))
被主sequence調(diào)用的從sequence也能帶參數(shù)，例如從sequence名字叫s2，主sequence名字叫s1:
sequence s1;
s2(a,b);
endsequence
4. property內(nèi)部可以定義局部變量，像正常的程序一樣。
property p1;
int cnt;
.....................
endproperty
【注】在介紹語法之前，先強(qiáng)調(diào)寫斷言的一般格式：
一般，斷言是基于時(shí)序邏輯的，單純進(jìn)行組合邏輯的斷言很少見，因?yàn)樘M(fèi)內(nèi)存（時(shí)序邏輯是每個(gè)時(shí)鐘周期判斷一次，而組合邏輯卻是每個(gè)時(shí)鐘周期內(nèi)判斷多次，內(nèi)存吃不消）。
因此，寫斷言的一般規(guī)則是： time + event，要斷定發(fā)生什么event，首先要指定發(fā)生event的時(shí)間，例如
每個(gè)時(shí)鐘上升沿 + 發(fā)生某事
某信號(hào)下降時(shí) + 發(fā)生某事
5. 語法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ā)c
6. 語法2：在“時(shí)序邏輯”中判斷獨(dú)立的一根信號(hào)的行為：
@ (posedge clk) A事件; ———— 當(dāng)clk上升沿時(shí)，如果發(fā)生A事件，斷言將報(bào)警。
邊沿觸發(fā)內(nèi)置函數(shù)：(假設(shè)存在一個(gè)信號(hào)a)
$rose( a );———— 信號(hào)上升
$fell( a );———— 信號(hào)下降
$stable( a );———— 信號(hào)值不變
7. 語法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ā)生后1~3個(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事件成立到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 a
b;
else
succeed;
因此，一旦 a 發(fā)生，b 必須發(fā)生，斷言才成功。如果a沒發(fā)生，走else，同樣成功。
(7) @ (posedge clk) a |=> b ———— 斷定clk上升沿后，a事件開始發(fā)生，下一個(gè)時(shí)鐘沿后，b事件開始發(fā)生。
(8) @ (posedge clk) a |=>##2b ———— 斷定clk上升沿后，a事件開始發(fā)生，下三個(gè)時(shí)鐘沿后，b事件開始發(fā)生。
(9) @ (posedge clk) $past(a,2) == 1'b1 ———— 斷定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ù)1~3個(gè)時(shí)鐘周期內(nèi)都成立。
@ (posedge clk) a [->3] ———— 斷定“@ (posedge clk) a”在非連續(xù)的3個(gè)時(shí)鐘周期內(nèi)都成立。
舉一個(gè)復(fù)雜點(diǎn)的例子：
property ABC;
int 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è)周期前b^2+1，再過3個(gè)周期，斷定信號(hào)d一定會(huì)起來，再過3個(gè)周期，信號(hào)d又起來一次。。。。。。。只有這些斷定都成功，該句斷言成功。otherwise，信號(hào)a從一開始就沒起來，則斷言也成功。
8. 語法4：多時(shí)鐘域聯(lián)合斷言：一句斷言可以表示多個(gè)時(shí)鐘域的信號(hào)關(guān)系，例如：
@ （posedge clk1） a |-> ##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) b
9. 語法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) $isunknown(BUS) ————BUS中存在高阻態(tài)或未知態(tài)。
(4) countones(BUS)==n ————BUS中有且僅有n bits是高，其他是低。
10. 語法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. 語法6：斷言覆蓋率檢測：
name: cover property (func_name)
11. 在modelsim中開啟斷言編譯和顯示功能：
（1）【編譯verilog代碼時(shí)按照system verilog進(jìn)行編譯】 vlog -sv abc.v
（2）【仿真命令加一個(gè)-assertdebug】 vsim -assertdebug -novopt testbench
（3）【如果想看斷言成功與否的分析，使用打開斷言窗口的命令】 view assertions
12. 在VCS中加入斷言編譯和顯示功能：
在fsdb文件中加一句話：$fsdbDumpSVA
在VCS編譯參數(shù)：system "vcs $VCS_SIMULATION" 中加入一些options:
-assert enable_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代碼的，不依賴測試案例，而是相對(duì)“靜態(tài)”。例如：我們要測試一個(gè)串行數(shù)據(jù)讀寫單元，數(shù)據(jù)線只有一根，先傳四位地址，再傳數(shù)據(jù)。
（1）案例驗(yàn)證法：寫一個(gè)地址，再寫一段數(shù)據(jù)，然后讀取該地址，看輸出的是不是剛才寫的數(shù)據(jù)。
（2）斷言法：不需要專門設(shè)計(jì)地址和數(shù)據(jù)，當(dāng)發(fā)起寫時(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語言的int和數(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)格：語法介紹的 “a |-> b”，實(shí)際上是 “if a, then b”的邏輯，當(dāng)a不發(fā)生，b也不會(huì)被判斷，該斷言自然成功。但當(dāng)我們的邏輯是
if a1
{
if a2
then 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<=a邏輯的斷言應(yīng)該是：“@ (posedge clk) (a==a,tmp=a) |=> (b==tmp);”
針對(duì)上述幾點(diǎn)，舉一個(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ù)組arr[4]，
//“@(posedge clk) !vld_pulse_r[0] && !DataIn”是真實(shí)的預(yù)備條件
//“##4 (read==read, arr[0] = DataIn)”只是為了在特定時(shí)間內(nèi)賦值，有用的語句是“arr[0] = DataIn”，//“read==read”是廢話，為了編譯通過。
//arr賦值完畢后，進(jìn)入function進(jìn)行處理，判斷實(shí)際地址addr跟junc處理過的數(shù)據(jù)是否相同。
//“addr == junc(arr[0],arr[1],arr[2],arr[3]);”就是junction調(diào)用。
property wr_p;
int arr[4];
@(posedge clk) !vld_pulse_r[0] && !DataIn
##4 (read==read, arr[0] = DataIn)
##1 (read==read, arr[1] = DataIn)
##1 (read==read, arr[2] = DataIn)
##1 (read==read, arr[3] = DataIn) |=>
addr == junc(arr[0],arr[1],arr[2],arr[3]);
endproperty
//////////////////////////////////////////////////////////////////////////
function [3:0] junc;
input a,b,c,d;
reg [3:0] a1;
reg [3:0] b1;
reg [3:0] c1;
reg [3:0] d1;
a1 = {3'b0,a};
b1 = {3'b0,b};
c1 = {3'b0,c};
d1 = {3'b0,d};
junc = a1+(b1<<1)+(c1<<2)+(d1<<3);
$display(junc);
endfunction
////////////////////////////////////////////////////////////////////////
7. 如果想在SVA中使用類似for(){....}的功能，別忘了語法中介紹的[*3]，這是在斷言中實(shí)現(xiàn)for的唯一方式。
##4 (廢話, cnt = 0, arr[cnt] = DataIn, cnt++) //初始化一下，
##1 (read==read, arr[cnt] = DataIn, cnt++)[*3] //循環(huán)3次
8. 每句斷言都是一個(gè)小程序：如上例，在##4時(shí)間點(diǎn)上，(廢話, cnt = 0, arr[cnt] = DataIn, cnt++)就是一個(gè)小程序，信號(hào)斷言必須是第一句，其他運(yùn)算按照順序進(jìn)行。
9. 斷言的變量除了可用C語言中的int，float外，還可以是reg [n:0]等數(shù)字電路類型。
10. 注意：
像這種寫法：
property ept_p;
@(posedge rd_clk) ((rd_num == 0) |-> rd_ept)
&& (rd_ept |-> (rd_num == 0));
endproperty
是錯(cuò)誤的，寫了|->，就不能再用 && 等事件組合邏輯了。
解決方法是使用2個(gè)斷言，沒更好的方法。