systemverilog-斷言-快速教程

8Bind:veryusefulinsystemverilog.Assertion:##“a##3b”意思是a之后3個(gè)周期b2．“|->”表示如果先行算子匹配，后序算子在同一周期開(kāi)始計(jì)算“|=>”表示如果先行算子匹配，后序算子在下一個(gè)周期開(kāi)始計(jì)算重復(fù)操作符：*連續(xù)重復(fù)“[*m]”:“a[*1:3]”表示a被連續(xù)重復(fù)1~3次**跳轉(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)警。一般在數(shù)字電路設(shè)計(jì)中都要加入斷言，斷言占整個(gè)設(shè)計(jì)的比例應(yīng)不少于30%。以下是斷言的語(yǔ)法：SVA的插入位置：在一個(gè).V文件中：moduleABC();rtl代碼SVA斷言endmodule注意：不要將SVA寫(xiě)在enmodule外面。斷言編寫(xiě)的一般格式是：【例】斷言名稱(chēng)1:assertproperty(事件1)〃沒(méi)有分號(hào)$display("",$time);//有分號(hào)else$display("",$time);//有分號(hào)斷言名稱(chēng)2:assertproperty(事件2)$display("",$time);else$display("",$time);斷言的目的是：斷定'事件1”和''事件2〃會(huì)發(fā)生，如果發(fā)生了，就記錄為pass，如果沒(méi)發(fā)生，就記錄為fail。注意：上例中沒(méi)有if，只有else，斷言本身就充當(dāng)if的作用。上例中，事件1和事件2可以用兩種方式來(lái)寫(xiě)：序列塊：sequeneename;ooooooooo;endsequenee屬性塊：propertyname;ooooooooo;endsequenee從定義來(lái)講，sequenee塊用于定義一個(gè)事件(磚)，而property塊用于將事件組織起來(lái)，形成更復(fù)雜的一個(gè)過(guò)程(樓)。sequenee塊的內(nèi)容不能為空，你寫(xiě)亂字符都行，但不能什么都沒(méi)有。sequenee也可以包含另一個(gè)sequenee,如：sequenees1;s2(a,b);endsequenee〃s1和s2都是sequenee塊sequenee塊和property塊都有name，使用assert調(diào)用時(shí)都是：'assertproperty(name);"在SVA中，sequenee塊一般用來(lái)定義組合邏輯斷言，而property—般用來(lái)定義一個(gè)有時(shí)間觀(guān)念的斷言，它會(huì)常常調(diào)用sequenee，一些時(shí)序操作如、'|->"只能用于property就是這個(gè)原因。注：以下介紹的SVA語(yǔ)法，既可以寫(xiě)在sequenee中，也可以寫(xiě)在property中，語(yǔ)法是通用的。帶參數(shù)的property、帶參數(shù)的sequeneeproperty也可以帶參數(shù)，參數(shù)可以是事件或信號(hào)，調(diào)用時(shí)寫(xiě)成：assertproperty(p1(a,b))被主sequenee調(diào)用的從sequenee也能帶參數(shù)，例如從sequenee名字叫s2，主sequenee名字叫s1:sequenees1;s2(a,b);endsequeneeproperty內(nèi)部可以定義局部變量，像正常的程序一樣。propertyp1;intent;endproperty【注】在介紹語(yǔ)法之前，先強(qiáng)調(diào)寫(xiě)斷言的一般格式：一般，斷言是基于時(shí)序邏輯的，單純進(jìn)行組合邏輯的斷言很少見(jiàn)，因?yàn)樘M(fèi)內(nèi)存(時(shí)序邏輯是每個(gè)時(shí)鐘周期判斷一次，而組合邏輯卻是每個(gè)時(shí)鐘周期內(nèi)判斷多次，內(nèi)存吃不消)。因此，寫(xiě)斷言的一般規(guī)則是：time+event，要斷定發(fā)生什么event，首先要指定發(fā)生event的時(shí)間，例如每個(gè)時(shí)鐘上升沿+發(fā)生某事某信號(hào)下降時(shí)+發(fā)生某事語(yǔ)法1：信號(hào)(或事件)間的''組合邏輯〃關(guān)系：常見(jiàn)的有：&&,||,!,人a和b哪個(gè)成立都行，但如果都成立，就認(rèn)為是a成立：firstmatch(a||b)，與“||”基本相同，不同點(diǎn)是當(dāng)a和b都成立時(shí)，認(rèn)為a成立。a?b:ca事件成功后，觸發(fā)b，a不成功則觸發(fā)c語(yǔ)法2:在'時(shí)序邏輯〃中判斷獨(dú)立的一根信號(hào)的行為：@(posedgeclk)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)值不變語(yǔ)法3:在'時(shí)序邏輯〃中判斷多個(gè)事件/信號(hào)的行為關(guān)系：intersect(a,b)斷定a和b兩個(gè)事件同時(shí)產(chǎn)生，且同時(shí)結(jié)束。awithinb斷定b事件發(fā)生的時(shí)間段里包含a事件發(fā)生的時(shí)間段。a##2b斷定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ā)生。cthroughout(a##2b)斷定在a事件成立到b事件成立的過(guò)程中，c事件''一直〃成立。@(posedgeclk)a|->b斷定clk上升沿后，a事件''開(kāi)始發(fā)生〃，同時(shí)，b事件發(fā)生。(6)@(posedgeelk)a.end|->b斷定elk上升沿后，a事件執(zhí)行了一段時(shí)間“結(jié)束〃后，同時(shí)，b事件發(fā)生。注："a|->b"在邏輯上是一個(gè)判斷句式，即：ifab；elsesucceed;因此，一旦a發(fā)生，b必須發(fā)生，斷言才成功。如果a沒(méi)發(fā)生，走else，同樣成功。@(posedgeelk)a|=>b斷定elk上升沿后，a事件開(kāi)始發(fā)生，下一個(gè)時(shí)鐘沿后，b事件開(kāi)始發(fā)生。@(posedgeelk)a匸>##2b斷定elk上升沿后，a事件開(kāi)始發(fā)生，下三個(gè)時(shí)鐘沿后，b事件開(kāi)始發(fā)生。@(posedgeelk)$past(a,2)==1'b1斷定a信號(hào)在2個(gè)時(shí)鐘周期''以前〃，其電平值是1。@(posedgeelk)a[*3]斷定“@(posedgeelk)a”在連續(xù)3個(gè)時(shí)鐘周期內(nèi)都成立。@(posedgeelk)a[*1:3]斷定“@(posedgeelk)a”在連續(xù)1~3個(gè)時(shí)鐘周期內(nèi)都成立。@(posedgeelk)a[->3]斷定“@(posedgeelk)a”在非連續(xù)的3個(gè)時(shí)鐘周期內(nèi)都成立。舉一個(gè)復(fù)雜點(diǎn)的例子：propertyABC;inttmp;@(posedgeelk)($rose(a),tmp=b)|->##4(e==(tmp*tmp+1))##3d[*3];endproperty上例的一個(gè)property說(shuō)明：當(dāng)elk上升沿時(shí)，斷言開(kāi)始。首先斷定信號(hào)a由低變高，將此時(shí)的信號(hào)b的值賦給變量tmp，4個(gè)時(shí)鐘周期后，斷定信號(hào)e的值是4個(gè)周期前b人2+1，再過(guò)3個(gè)周期，斷定信號(hào)d一定會(huì)起來(lái)，再過(guò)3個(gè)周期，信號(hào)d又起來(lái)一次。。。。。。。只有這些斷定都成功，該句斷言成功。otherwise，信號(hào)a從一開(kāi)始就沒(méi)起來(lái)，則斷言也成功。語(yǔ)法4:多時(shí)鐘域聯(lián)合斷言：一句斷言可以表示多個(gè)時(shí)鐘域的信號(hào)關(guān)系，例如：@(posedgeelkl)a|->##1@(posedgeelk2)b當(dāng)clkl上升沿時(shí)，事件a發(fā)生，緊接著如果過(guò)來(lái)第二個(gè)時(shí)鐘Clk2的上升沿，則b發(fā)生。、'##1”在跨時(shí)鐘時(shí)不表示一個(gè)時(shí)鐘周期，只表示等待最近的一個(gè)跨時(shí)鐘事件。所以此處不能寫(xiě)成##2或其他。但是可以寫(xiě)成：@(posedgeclkl)a|=>@(posedgeclk2)b語(yǔ)法5:總線(xiàn)的斷言函數(shù)總線(xiàn)就是好多根bit線(xiàn)，共同表示一個(gè)數(shù)。SVA提供了多bit狀態(tài)一起判斷的函數(shù)，即總線(xiàn)斷言函數(shù)：⑴$onehot(BUS)BUS中有且僅有1bit是高，其他是低。$onehotO(BUS)BUS中有不超過(guò)1bit是高，也允許全0。$isunknown(BUS)BUS中存在高阻態(tài)或未知態(tài)。countones(BUS)==nBUS中有且僅有nbits是高，其他是低。語(yǔ)法6:屏蔽不定態(tài)當(dāng)信號(hào)被斷言時(shí)，如果信號(hào)是未復(fù)位的不定態(tài)，不管怎么斷言，都會(huì)報(bào)告：''斷言失敗〃，為了在不定態(tài)不報(bào)告問(wèn)題，在斷言時(shí)可以屏蔽。如：@(posedgeclk)(q==$past(d))，當(dāng)未復(fù)位時(shí)報(bào)錯(cuò)，屏蔽方法是將該句改寫(xiě)為：@(posedgeclk)disable肝(!rst_n)(q==$past(d))〃rst是低電平有效語(yǔ)法6:斷言覆蓋率檢測(cè)：name:coverproperty(func_name)在modelsim中開(kāi)啟斷言編譯和顯示功能：(1)【編譯verilog代碼時(shí)按照systemverilog進(jìn)行編譯】vlog-svabc.v(2)【仿真命令加一^-assertdebug】vsim-assertdebug-novopttestbench(3)【如果想看斷言成功與否的分析，使用打開(kāi)斷言窗口的命令】viewassertions在VCS中加入斷言編譯和顯示功能：在fsdb文件中加一句話(huà)：$fsdbDumpSVA在VCS編譯參數(shù)：system"vcs$VCS_SIMULATION"中加入一些options:-assertenable_diag\-assertvpiSeqBeginTime\-assertvpiSeqFail\-assertreport=路徑\-assertfinish_maxfail=100【經(jīng)驗(yàn)】以下是一些編寫(xiě)斷言的經(jīng)驗(yàn)：斷言的目的：傳統(tǒng)的驗(yàn)證方法是通過(guò)加激勵(lì)，觀(guān)察輸出。這種方法對(duì)案例的依賴(lài)嚴(yán)重，案例設(shè)計(jì)不好，問(wèn)題不便于暴露。而斷言是伴隨RTL代碼的，不依賴(lài)測(cè)試案例，而是相對(duì)“靜態(tài)〃。例如：我們要測(cè)試一個(gè)串行數(shù)據(jù)讀寫(xiě)單元，數(shù)據(jù)線(xiàn)只有一根，先傳四位地址，再傳數(shù)據(jù)。（1）案例驗(yàn)證法：寫(xiě)一個(gè)地址，再寫(xiě)一段數(shù)據(jù)，然后讀取該地址，看輸出的是不是剛才寫(xiě)的數(shù)據(jù)。（2）斷言法：不需要專(zhuān)門(mén)設(shè)計(jì)地址和數(shù)據(jù)，當(dāng)發(fā)起寫(xiě)時(shí)，在地址傳輸?shù)臅r(shí)間里將地址存儲(chǔ)到一個(gè)變量里，在數(shù)據(jù)傳輸?shù)臅r(shí)間里將數(shù)據(jù)存儲(chǔ)到一個(gè)變量里，觀(guān)察RAM中該地址是否存在該數(shù)據(jù)就可以了。斷言設(shè)計(jì)相當(dāng)于在電腦上把RTL實(shí)現(xiàn)的功能再實(shí)現(xiàn)一遍。斷言中可以包含function和task。而且function經(jīng)常用于斷言，因?yàn)橛械奶幚砗軓?fù)雜，而斷言又是''一句式〃的，無(wú)法分成好幾句進(jìn)行表達(dá)，所以需要function替斷言分擔(dān)工作。斷言允許規(guī)定同時(shí)發(fā)生的事件，就是組合邏輯，你可以寫(xiě)成：a&&b，也可以寫(xiě)成a##0b，不能寫(xiě)##0.5，不支持小數(shù)。斷言是用電腦模仿RTL的運(yùn)行過(guò)程，當(dāng)RTL功能復(fù)雜時(shí)，你必須用到變量。斷言中支持C語(yǔ)言的int和數(shù)組聲明，但在賦值時(shí)“不能"寫(xiě)成：##4var=Signal，其中var是斷言中的變量，和RTL無(wú)關(guān)，Signal是RTL中的一個(gè)信號(hào)。本句是想在第4周期將Signal的值賦給var，以便在后面使用該值。但本句只有變量賦值，沒(méi)有對(duì)RTL信號(hào)的任何斷言，就會(huì)報(bào)錯(cuò)，解決方法是：##4（“廢話(huà)"，var=Signal），一定要有斷言的話(huà)我們就寫(xiě)'廢話(huà)"，例如:data==data等。如果有多個(gè)變量要賦值也可以，##4（廢話(huà)，變量1賦值，變量2賦值）關(guān)于斷言的表達(dá)風(fēng)格：語(yǔ)法介紹的“a|->b〃，實(shí)際上是“ifa,thenb〃的邏輯，當(dāng)a不發(fā)生，b也不會(huì)被判斷，該斷言自然成功。但當(dāng)我們的邏輯是ifal{ifa2thenb}該如何用斷言表達(dá)？？？？或許可以寫(xiě)成：“a1|->a2|->b〃，也可以，但常用的表達(dá)是：“a1&&a2|->b”或者“a1##3a2|->b”關(guān)于斷言的時(shí)序：時(shí)序邏輯的斷言需要注意的一個(gè)問(wèn)題：例如：假設(shè)當(dāng)elk上升沿到來(lái)時(shí)，b<=a。將上述邏輯寫(xiě)成斷言時(shí)，如果寫(xiě)成'@(posedgeelk)b==a〃，看起來(lái)和b<=a一樣，但實(shí)際上是錯(cuò)的。因?yàn)楫?dāng)時(shí)鐘上升時(shí)，b還沒(méi)有得到a的值，a還需要一段保持時(shí)間。即，斷言中的信號(hào)值實(shí)際上是時(shí)鐘沿到來(lái)之前的值，而不是時(shí)鐘沿到來(lái)后他們將要編程的值。所以，b<=a邏輯的斷言應(yīng)該是：“@(posedgeelk)(a==a,tmp=a)|=>(b==tmp);"針對(duì)上述幾點(diǎn)，舉一個(gè)復(fù)雜的例子：斷言wr的功能是檢查串行地址輸入是否正確，串行地址輸入線(xiàn)是Dataln。$time返回值以0.1ns為單位(因?yàn)槲以趖estbench中的單位規(guī)定是'timescale1ns/100ps，精度是100ps=0.1ns)，所以$time/10才是ns。/////////////////////////////////////////////////////////////////////////////wr:assertproperty(wr_p)$display("succeed:",$time/10);else$display("error:",$time/10);/////////////////////////////////////////////////////////////////////////////〃斷言可以聲明一個(gè)int數(shù)組arr[4]，〃“@(posedgeclk)!vld_pulse_r[O]&&!DataIn‘是真實(shí)的預(yù)備條件//“##4(read==read,arr[0]=DataIn)”只是為了在特定時(shí)間內(nèi)賦值，有用的語(yǔ)句是、arr[0]=DataIn”，〃“read==read"是廢話(huà)，為了編譯通過(guò)。//arr賦值完畢后，進(jìn)入function進(jìn)行處理，判斷實(shí)際地址addr跟junc處理過(guò)的數(shù)據(jù)是否相同。//“addr==junc(arr[0],arr[1],arr[2],arr[3]);‘就是junction調(diào)用。propertywr_p;intarr[4];@(posedgeclk)!vld_pulse_r[O]&&!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///////////////