sva_assertion: 15道助力飛升的斷言練習(xí)

前言

紙上得來終覺淺，絕知此事要躬行。把之前學(xué)習(xí)到的15道并行斷言練習(xí)整理好拿出來助大家一同飛升，相信我，練完之后再也沒有難得住你的斷言了，你就信吧！每道題都遵循著題目-解析-答案-驗(yàn)證四個(gè)步驟進(jìn)行，除非太簡單了可能會(huì)省去解析或者驗(yàn)證的過程。

省流版在最后，直接看最后一題！

練習(xí)1

題目

系統(tǒng)復(fù)位后，狀態(tài)機(jī)信號(hào)status在任意一拍均有且只有1bit信號(hào)有效。

分析

每一拍都要檢查，因此不需要前置蘊(yùn)含算子了（蘊(yùn)含算子即|->和|=>）；均有且只有1比特信號(hào)有效意味著我們需要使用系統(tǒng)函數(shù)$onehot()；復(fù)位之后檢查我們需要用到disable iff語句；

答案

property assert_chk；
    @(posedge clk) disable iff(~rst_n)
        $onehot(status);
endproperty
assert_test: assert property(assert_chk); //這行之后就省略了哈

驗(yàn)證

注意嗷，對(duì)于onehot函數(shù)，status全0也是不行的哈。

"/home/ICer/test.sv", 484: testbench.u_test.assert_test: started at 335000ps failed at 335000ps
Offending '$onehot(status)'
"/home/ICer/test.sv", 484: testbench.u_test.assert_test: started at 345000ps failed at 345000ps
Offending '$onehot(status)'
$finish called from file "../top/testbench.sv", line 35.

練習(xí)2

題目

系統(tǒng)復(fù)位后，data信號(hào)在任何時(shí)刻均不能為X態(tài)或Z態(tài)。

分析

和上一個(gè)題目類似，可以直接調(diào)用系統(tǒng)函數(shù)，注意是不能為X態(tài)或Z態(tài)。

答案

property assert_chk;
    @(posedge clk) disable iff(~rst_n)
        ~$isunkonwn(data);
endproperty

太簡單了，就不進(jìn)行仿真確認(rèn)了哈。

練習(xí)3

題目

某一奇怪的握手協(xié)議中規(guī)定，vld信號(hào)只能在ready信號(hào)有效期間有效。

分析

簡單來說可以反向思考，其實(shí)就是任何一拍vld是有效的，那么ready信號(hào)也必須是有效的，因此我們可以使用蘊(yùn)含算子|->在vld有效時(shí)候檢查ready是否為有效態(tài)。

答案

property assert_chk;
    @(posedge clk) disable iff(~rst_n)
        vld |-> ready;
endproperty

練習(xí)4

題目

接口data_vld有效時(shí)，data信號(hào)值必須處于合理的范圍內(nèi)（假設(shè)合理范圍時(shí)‘h0000~'h7FFF）。

分析

data信號(hào)值處于合理范圍需要用到inside方法，他本身就是檢查一個(gè)值是否處于之后的范圍內(nèi)。

答案

property assert_chk;
    @(posedge clk) disable iff(~rst_n)
        data_vld |-> (data inside{['h0:'h7FFF]});
endproperty

驗(yàn)證

"/home/ICer/test.sv", 490: testbench.u_test.assert_test: started at 505000ps failed at 505000ps
Offending '(data inside {['b0:'h00007fff]})'
"/home/ICer/test.sv", 490: testbench.u_test.assert_test: started at 515000ps failed at 515000ps
Offending '(data inside {['b0:'h00007fff]})'
$finish called from file "../top/testbench.sv", line 35.

練習(xí)5

題目

data_vld是一個(gè)檢測上升沿的單拍脈沖信號(hào)，最多有效1拍就會(huì)拉低等待下次觸發(fā)。

分析

其實(shí)就是說data_vld如果這一拍為1，那么下一拍一定為0，那么我們只需要在data_vld==1時(shí)檢查下一拍是不是0就可以了，可以使用|=>也可以使用|-> ##1。

答案

property assert_chk;
    @(posedge clk) disable iff(~rst_n)
        data_vld |=> ~data_vld;
endproperty

練習(xí)6

題目

單比特信號(hào)data_vld連續(xù)有效時(shí)間跨度最多為5拍。

分析

要檢查vld信號(hào)每次為1應(yīng)該持續(xù)[1:5]拍，想想什么操作符是連續(xù)持續(xù)n拍呢？a[*n]：連續(xù)重復(fù)運(yùn)算符，a[*2:4]含義為a信號(hào)重復(fù)2~4拍。不如我們先寫一個(gè)簡單的，如果規(guī)定vld有效必須為5拍，那么我們?cè)趺磳懩兀窟@里肯定要用到$rose和$fell函數(shù)了，因?yàn)槌掷m(xù)幾拍肯定是從頭數(shù)到尾我們需要上升沿和下降沿；持續(xù)幾拍那就用到了我們連續(xù)重復(fù)了[*m:n]，那我們先寫一個(gè)看看：

property assert_chk;
    @(posedge clk) disable iff(~rst_n)
        $rose(data_vld) |-> data_vld[*5] ##0 $fell(data_vld);
endproperty

看上去挺合理的，data_vld有效開始檢查，到data_vld無效時(shí)結(jié)束，在這期間data_vld連續(xù)有效了5拍，如果不是5拍就報(bào)錯(cuò)。不過這樣寫是有問題的，問題請(qǐng)見下面的波形，這很明顯是一個(gè)維持了5拍的信號(hào)對(duì)吧：

注意開始檢查的時(shí)刻是60ns，此時(shí)data_vld采樣值為1與上一拍0滿足了$rose，同時(shí)由于我們使用了|->符號(hào)單拍開始檢查，所以data_vld在60ns出重復(fù)為1次；接下來80ns處連續(xù)重復(fù)了第2次，100ns處重復(fù)第3次，120ns處重復(fù)第4次，140ns處重復(fù)第5次，好的在140ns處data_vld[*5]匹配完成；接下來匹配##0 $fell(data_vld)，##0含義為當(dāng)拍就要看，那么當(dāng)拍data_vld值為1上一拍也是1，$fell匹配失敗，斷言也就失敗了。

因此這樣的寫法是不正確的，會(huì)把一個(gè)符合預(yù)期的行為誤判為斷言失敗，所以我們修改一下成下面這樣：

property assert_chk;
    @(posedge clk) disable iff(~rst_n)
        $rose(data_vld) |-> data_vld[*5] ##1 $fell(data_vld);
endproperty

變成##1就好啦，在data_vld[*5]的下一拍來檢查$fell，完美的解決了這個(gè)問題，這個(gè)用法一定要牢記。

再來思考一個(gè)問題，如果不用$rose(data_vld) |-> data_vld[*5] ##1 $fell(data_vld)而改成data_vld |-> data_vld[*5] ##1 $fell(data_vld）會(huì)有什么后果，反正都是再data_vld有效時(shí)候開始檢查嘛；后果就是本來只在60ns處開始一條檢查線程，現(xiàn)在會(huì)在60ns、80ns、100ns、120ns和140ns處開了多條檢查線程，而后面這些線程顯然是一定失敗的也不是我們需要檢查的。

那么回到題目本身，其實(shí)也就很好解決了，只需要把[*5]修改為[*1:5]就契合了題目要求。

答案

property assert_chk;
    @(posedge clk) disable iff(~rst_n)
        $rose(data_vld) |-> data_vld[*1：5] ##1 $fell(data_vld);
endproperty

驗(yàn)證

data_vld分別持續(xù)了5拍、4拍、6拍的波形：

assert pass case!!!
assert pass case!!!
"/home/ICer/test.sv", 488: testbench.u_test.assert_test: started at 995000ps failed at 1045000ps
Offending '$fell(data_vld)'
assert fail case!!!
$finish called from file "../top/testbench.sv", line 35.

練習(xí)7

題目

req信號(hào)（單拍脈沖）有效之后（含當(dāng)拍），rsp信號(hào)有效之前（含當(dāng)拍），必須要收到（出現(xiàn)）4次data_vld有效。

分析

這個(gè)題目和上一個(gè)題有點(diǎn)類似，我們來分析一下。這個(gè)斷言應(yīng)該在req有效當(dāng)拍開始而在rsp有效（第一次有效）時(shí)結(jié)束，我們關(guān)注的就是req->rsp之間的事情。所以很顯然前置算子就是req（因?yàn)槭菃闻男盘?hào)，所以不需要用$rose）。后面怎么寫呢？我們可以使用intersect + [->1]的句式，a [->n]：非連續(xù)跟隨重復(fù)符，或者叫g(shù)o-to重復(fù)符，含義是a非連續(xù)(就是無所謂連不連續(xù))重復(fù)n次，只在第n次重復(fù)時(shí)刻點(diǎn)匹配（跟隨的含義）。最常用的a [->1]等價(jià)于(!a) [*0:$] ##1 a，也就是匹配了a序列第一次成立的時(shí)刻。

intersect運(yùn)算符是最重要的一個(gè)運(yùn)算符，intersect和and有一些類似，都是連接兩個(gè)事件，兩個(gè)事件均成功整個(gè)匹配才成功。不過intersect多了一個(gè)條件，那就是兩個(gè)事件必須在同一時(shí)刻結(jié)束。換句話說a intersect b能匹配成功，a、b兩個(gè)序列的長度必須相等。

先把答案寫下來，再分析下：

property vld_chk;
    @(posedge clk) disable iff(~rst_n)
        req |-> data_vld[=4] intersect (rsp[->1]);
endproperty

intesect連接的兩個(gè)序列必須等長，那么后面的ack[->1]持續(xù)的時(shí)間段時(shí)哪里呢？從下圖的波形中可以看出時(shí)從前置算子匹配成功的60ns到ack信號(hào)第一次為高有效的220ns處；因此通過這樣的句式就成功的限制住了data_vld高有效4次這一事件必須也發(fā)生在60ns~220ns之間，即從req有效當(dāng)拍到ack有效當(dāng)拍；這個(gè)句式事實(shí)上時(shí)非常常見的寫法。

答案

property vld_chk;
    @(posedge clk) disable iff(~rst_n)
        req |-> data_vld[=4] intersect (rsp[->1]);
endproperty

驗(yàn)證

第一段成功了，第二段是斷言失敗。

assert pass case!!!
"/home/ICer/test.sv", 488: testbench.u_test.assert_test: started at 955000ps failed at 1005000ps
Offending 'data_vld'
assert fail case!!!
$finish called from file "../top/testbench.sv", line 35.

練習(xí)8

題目

req信號(hào)（單拍脈沖）有效之后（不含當(dāng)拍從下一拍開始），rsp信號(hào)有效之前（不含當(dāng)拍，rsp有效之前），必須要收到（出現(xiàn)）4次data_vld有效。

分析

和上一個(gè)問題非常相似，我們繼續(xù)來解決一下，其實(shí)核心好事data_vld[=4]這個(gè)序列發(fā)生在哪個(gè)時(shí)間段的問題。req的下一拍開始，那么我們可以使用|=>或者|->##1，這兩個(gè)是都可以的；ack有效的前一拍data_vld[=4]要匹配完成，要怎么處理呢？可以采用這種形式（data_vld[=4] ##1 1'b1），由于1'b1是一個(gè)恒成立的序列，這樣寫的效果就是data_vld[=4]匹配成功點(diǎn)往后推遲了一拍。

property assert_chk;
    @(posedge clk) disable iff(~rst_n)
        req |-> ##1 (data_vld[=4] ##1 1'b1) intersect (rsp[->1]);
endproperty

我們還是以波形來理解，先看一個(gè)成功的波形。前置算子req在60ns匹配成功，|-> ##1意味著從下一拍開始進(jìn)行后續(xù)的判定。黃色箭頭220ns處rsp[->1]匹配成功，這意味著（data_vld[=4] ##1 1'b1）序列必須在80ns~220ns間匹配完成，而在data_vld[=4]在200ns藍(lán)色箭頭處匹配成功，因此（data_vld[=4] ##1 1'b1）在220ns匹配成功，斷言成功。

下面看一個(gè)失敗的例子，rsp[->1]在220ns匹配成功，而（data_vld[=4] ##1 1'b1）在哪里匹配成功呢？在240ns處才匹配成功（換句話說，在220ns處剛剛匹配到data_vld[=3] ##1 1'b1成功），因此最后斷言失敗。

再看一個(gè)略帶迷惑性的例子，如下圖這個(gè)行為最后斷言是會(huì)報(bào)成功還是失敗呢？我和同學(xué)有一些爭論，不過我認(rèn)為是會(huì)成功的，因?yàn)樵?20ns時(shí)（data_vld[=4] ##1 1'b1）報(bào)匹配成功，rsp[->1]在220ns處報(bào)匹配成功，intersect前后序列等長斷言匹配成功，檢查也就此結(jié)束。不過你說在220ns處data_vld[=5]了，那沒關(guān)系因?yàn)椋╠ata_vld[=5] ##1 1'b1）作為一個(gè)整體在240ns才匹配此時(shí)我的斷言都已經(jīng)檢查完成了，等待下一次req有效才會(huì)開始下一次檢查，因此對(duì)斷言成功沒有影響。

答案

property assert_chk;
    @(posedge clk) disable iff(~rst_n)
        req |-> ##1 (data_vld[=4] ##1 1'b1) intersect (rsp[->1]);
endproperty

驗(yàn)證

四段波形，分別是成功，失敗，失敗，成功。

assert pass case!!!
"/home/ICer/test.sv", 510: testbench.u_test.assert_test: started at 665000ps failed at 805000ps
Offending 'rsp'
assert fail case!!!
"/home/ICer/test.sv", 510: testbench.u_test.assert_test: started at 915000ps failed at 965000ps
Offending 'rsp'
assert fail case!!!
assert pass case!!!
$finish called from file "../top/testbench.sv", line 35.

練習(xí)9

題目

上一個(gè)題的變種，稍有變化。n_ready是維持信號(hào)，在n_ready有效期間，data_vld信號(hào)有效的次數(shù)應(yīng)該小于等于4次，data_vld信號(hào)為離散信號(hào)。

分析

這也是實(shí)際中很常見的場景，當(dāng)后級(jí)模塊的n_ready信號(hào)拉起時(shí)，一般表示后級(jí)模塊已經(jīng)不能接收更過的數(shù)據(jù)了，這個(gè)時(shí)候作為前級(jí)模塊應(yīng)該盡快停止數(shù)據(jù)的發(fā)送，不過鑒于前級(jí)模塊一般需要一些反應(yīng)的時(shí)間因此后級(jí)模塊允許再發(fā)送幾個(gè)數(shù)據(jù)過去（所謂的過沖），在本題目中這個(gè)數(shù)量最大為4個(gè)，也就是說0~4個(gè)都是可以接收的。

注意n_ready是維持信號(hào)，因此我們選取前置算子時(shí)候要選取的是n_ready的上升沿$rose(n_ready)；我們?nèi)耘f選擇intersect+[->1]的組織形式，那么后面跟的應(yīng)該是!n_ready[->1]即檢查結(jié)束點(diǎn)為n_ready無效的時(shí)刻，因此也可以寫成$fell(n_ready)[->1]，[->1]這個(gè)意思就是第一次成功的意思哈。初步組織斷言為：

property assert_chk;
    @(posedge clk) disable iff(~rst_n)
        $rose(n_ready) |-> (data_vld[=0:4]) intersect ($fell(n_ready)[->1]);
endproperty

不過還是老問題，這樣寫會(huì)發(fā)生誤判下面這種情況，可以看到下圖中n_ready有效期間data_vld有效了4拍這是完全符合要求的，不過會(huì)被上面斷言誤判為失敗，原因還是在于intersect后面的$fell(n_ready)是在220ns處匹配完成匹配的而不是200ns，因此220ns處的data_vld有效也會(huì)被計(jì)入因此斷言會(huì)判定data_vld[=5]，導(dǎo)致斷言失敗。

要避免這一個(gè)問題還是要用到上個(gè)練習(xí)的方法，引入##1 1'b1（還是直接理解成把序列匹配的時(shí)間點(diǎn)往后推一拍），這樣在220ns處(data_vld[0:4] ##1 1'b1)處于匹配成功的時(shí)間點(diǎn)，整個(gè)斷言判定成功。220ns處的data_vld就被這個(gè)##1 1'b1給推出去了。

答案

property assert_chk;
    @(posedge clk) disable iff(~rst_n)
        $rose(n_ready) |-> (data_vld[=0:4] ##1 1'b1) intersect ($fell(n_ready)[->1]);
endproperty

驗(yàn)證

assert pass case!!!
"/home/ICer/test.sv", 510: testbench.u_test.assert_test: started at 565000ps failed at 725000ps
Offending '$fell(n_ready)'
assert fail case!!!
$finish called from file "../top/testbench.sv", line 35.

練習(xí)10

題目

req信號(hào)（單拍脈沖信號(hào)）有效之后，rsp信號(hào)（單拍脈沖信號(hào)）有效之前（含當(dāng)拍），req信號(hào)不能再次有效，如下圖為合理情況的波形：

分析

這其實(shí)也是系統(tǒng)中比較常見的一個(gè)場景，那么我們來組織一下斷言；從前置算子入手，因?yàn)檎f了req是單拍脈沖信號(hào)所以前置算子可以直接寫req了；后面要斷的是什么呢？是在rsp[->1]之前req不能為1，所以可以使用intersect (rsp[->1])句式，寫成~req intersect (rsp[->1])；我們觀察下intersect前面是一個(gè)信號(hào)表達(dá)式，那么就跟前面我寫的東西連上了，這里也可以用throughout來連接等長的表達(dá)式與序列；而要使用|->還是|=>來連接呢？必須使用|=>來連接的，因?yàn)槟銖牟荒茉趓eq有效的當(dāng)拍斷言檢查req無效吧？

答案

property assert_chk;
    @(posedge clk) disable iff(~rst_n)
        req |=> ~req throughout (rsp[->1]);
endproperty

驗(yàn)證

assert pass case!!!
"/home/ICer/test.sv", 510: testbench.u_test.assert_test: started at 485000ps failed at 535000ps
Offending '(~req)'
assert fail case!!!
$finish called from file "../top/testbench.sv", line 35.

練習(xí)11

題目

某個(gè)模塊接收前級(jí)模塊發(fā)送的請(qǐng)求req，請(qǐng)求以req_id作為標(biāo)記，本模塊以rep和rep_id作為響應(yīng)信號(hào)表示已經(jīng)接收到請(qǐng)求；請(qǐng)檢查req和req_id有效后，最近的一拍rsp有效時(shí)rsp_id等于req_id。

分析

這個(gè)問題中遇到一個(gè)難點(diǎn)，就是我要判斷rsp_id是不是跟上一個(gè)req_id一樣，那么我就必須想辦法把reg_id保存下來；SVA提供了這樣的方法，我們直接用就可以了，我們可以在斷言中定義局部變量用來保存數(shù)據(jù)以備之后檢查使用，注意這個(gè)局部變量只在斷言期間有效，無法在斷言外使用。

確定一下前置算子，在什么情況下我們需要檢查呢，就是在req有效后最近的那一拍rsp有效時(shí)，我們需要觸發(fā)斷言檢查，“最近的那一拍”自然就時(shí)req后rsp第一次為1的時(shí)間點(diǎn)，因此使用req ##1 rsp[->1]來尋找這個(gè)時(shí)間點(diǎn)（這里我默認(rèn)rsp至少比req晚一拍），前置算子有了自然就可以完整的組織斷言，注意解答中的tmp_id就是斷言中可以使用的臨時(shí)變量。

答案

property assert_chk;
    reg [3:0] tmp_id;
    @(posedge clk) disable iff(~rst_n)
        (req,tmp_id = req_id) ##1 (rsp[->1]) |-> (rsp_id == tmp_id);
endproperty

驗(yàn)證

assert pass case!!!
"/home/ICer/test.sv", 510: testbench.u_test.assert_test: started at 655000ps failed at 765000ps
Offending '(rsp_id == tmp_id)'
assert fail case!!!
$finish called from file "../top/testbench.sv", line 35.

練習(xí)12

題目

某個(gè)模塊接收前級(jí)模塊發(fā)送的請(qǐng)求req，請(qǐng)求以req_id作為標(biāo)記，本模塊以rep和rep_id作為響應(yīng)信號(hào)表示已經(jīng)接收到請(qǐng)求；請(qǐng)檢查req有效后，下一次req有效時(shí)req_id為上一次req_id加1（0~FF~0循環(huán)發(fā)送id）。

分析

跟上一個(gè)題目幾乎是一毛一樣的，直接解答就好了。

答案

property assert_chk;
    reg [7:0] tmp_id
    @(posedge clk) disable iff(~rst_n)
        (req,tmp_id = req_id) ##1 (req[->1]) |-> (req_id == tmp_id+1);
endproperty

練習(xí)13

題目

某個(gè)模塊接收前級(jí)模塊發(fā)送的請(qǐng)求req，請(qǐng)求以req_id作為標(biāo)記，本模塊以rep和rep_id作為響應(yīng)信號(hào)表示已經(jīng)接收到請(qǐng)求；某個(gè)id被本模塊相應(yīng)前，不應(yīng)該再收到相同id的req請(qǐng)求。

分析

不用分析，使用intersect或者throughout都可以。

答案

property assert_chk;
    reg [7:0] tmp_id
    @(posedge clk) disable iff(~rst_n)
        (req,tmp_id = req_id) |=> ~(req && req_id==tmp_id) throughout (rsp && rsp_id==tmp_id)[->1];
endproperty

驗(yàn)證

4'hB的req還沒回，又發(fā)過來一個(gè)同樣id的請(qǐng)求，報(bào)錯(cuò)了。

"/home/ICer/test.sv", 510: testbench.u_test.assert_test: started at 405000ps failed at 475000ps
Offending '(~(req && (req_id == tmp_id)))'
$finish called from file "../top/testbench.sv", line 35.

練習(xí)14

題目

某模塊與兩個(gè)前級(jí)模塊對(duì)接，前級(jí)模塊1發(fā)送請(qǐng)求req1和req1_id，前級(jí)模塊2發(fā)送請(qǐng)求req2和req2_id，當(dāng)該模塊在同一拍收到兩個(gè)前級(jí)模塊的請(qǐng)求且req_id一致時(shí)，需要保證首先對(duì)前級(jí)模塊1進(jìn)行響應(yīng)。

分析

直接解答吧。

答案

property assert_chk;
    reg [7:0] tmp_id;
    @(posedge clk) disable iff(~rst_n)
        (req1 & req2 & req1_id==req2_id, tmp_id = req1_id) |=> ~(rsp2 && rsp2_id==tmp_id) throughout (rsp1 && rsp1_id==tmp_id)[->1];
endproperty

驗(yàn)證

"/home/ICer/test.sv", 510: testbench.u_test.assert_test: started at 405000ps failed at 435000ps
Offending '(~(rsp2 && (rsp2_id == tmp_id)))'
$finish called from file "../top/testbench.sv", line 35.

練習(xí)15

題目

hazard（或者稱bypass）讀取。在對(duì)SDRAM進(jìn)行數(shù)據(jù)讀取，如果在第1拍發(fā)起讀操作，需要在第4拍得到讀取數(shù)據(jù)；如果在這4拍內(nèi)有對(duì)相同地址的寫入操作，那么我們需要使用最新的寫入值作為讀操作的返回值（也就是常說的mem讀取hazard處理）；舉例如下圖，60ns發(fā)起讀操作120ns返回?cái)?shù)據(jù)（均以上升沿實(shí)際采樣為準(zhǔn)），在這期間如果沒有對(duì)同一地址的寫入操作，那么將返回從sdram中讀取的數(shù)據(jù)，如果有的話如下圖60ns和100ns時(shí)均有對(duì)同一地址的寫入操作，那么我們必然應(yīng)該回讀最新的寫入值即100ns時(shí)刻寫入的20；注意由于要求hazard 4拍，那么在60ns~120ns期間發(fā)生的同一地址寫操作均需要檢查進(jìn)去。

分析

這個(gè)問題是我學(xué)到的最難的斷言了，看起來簡單做起來完全沒有思緒的那一種。直接來思考有點(diǎn)轉(zhuǎn)不過彎來，不如我們分四種場景來檢查先：對(duì)第0拍繼續(xù)hazard、對(duì)第1拍繼續(xù)hazard、對(duì)第2拍繼續(xù)hazard和對(duì)第3拍繼續(xù)hazard。

1.什么時(shí)候我們需要對(duì)第0拍繼續(xù)hazard呢？條件就是第0拍有對(duì)同一地址的寫入，且之后的3拍沒有同一地址的寫入，那么讀回?cái)?shù)據(jù)必須是第0拍寫入的數(shù)據(jù)，波形示意如下：

根據(jù)描述我們可以寫出斷言如下，結(jié)合波形具體做一下解釋；rd_en有效即對(duì)應(yīng)波形中的60ns時(shí)刻，由于只對(duì)同一地址進(jìn)行hazard因此我們需要記錄一下地址（當(dāng)拍的這種其實(shí)不記錄也行，主要為了和后面一致）；##0表示當(dāng)拍，當(dāng)拍有wr_en&wr_addr=tmp_addr的話說明這個(gè)數(shù)據(jù)我們有可能進(jìn)行hazard所以也得保留下來；要繼續(xù)滿足什么條件呢，要滿足從下一拍開始連續(xù)3拍不能有wr_en&wr_addr=tmp_addr這個(gè)事出現(xiàn)，否則我們就要hazard后面最新的一拍嘛，因此寫上##1 ~(wr_en & wr_addr==tmp_addr)[*3]，注意因?yàn)?#1和[*3]的作用，時(shí)間點(diǎn)已經(jīng)來到了120ns；如果前置算子的條件滿足了，那么我們只需要在120ns當(dāng)拍檢查回讀數(shù)據(jù)rd_data==tmp_data是否成功就可以了，tmp_data就是我們之前記錄的第0拍的同一地址寫入數(shù)據(jù)嘛；好的因此第一種情況我們寫出來了，這個(gè)斷言是必須要滿足的。

property assert_chk;
    reg [31:0] tmp_data;
    reg [31:0] tmp_addr;
    @(posedge clk) disable iff(~rst_n)
        (rd_en, tmp_addr=rd_addr) ##0 (wr_en & wr_addr==tmp_addr, tmp_data=wr_data) ##1 ~(wr_en & wr_addr==tmp_addr)[*3] |-> rd_data==tmp_data;
endproperty

2.什么時(shí)候我們需要對(duì)第1拍繼續(xù)hazard呢？條件就是第1拍有對(duì)同一地址的寫入（顯然第0拍有沒有已經(jīng)不重要了或者說不必關(guān)心了），且之后的2拍沒有同一地址的寫入，那么讀回?cái)?shù)據(jù)必須是第1拍寫入的數(shù)據(jù)，波形示意如下：

rd_en有效即對(duì)應(yīng)波形中的60ns時(shí)刻，由于只對(duì)同一地址進(jìn)行hazard因此我們需要記錄一下地址，下一拍有wr_en&wr_addr=tmp_addr的話說明這個(gè)數(shù)據(jù)我們有可能進(jìn)行hazard所以保留下來；要繼續(xù)滿足從下一拍開始連續(xù)2拍不能有wr_en&wr_addr=tmp_addr這個(gè)事出現(xiàn)，因此寫上##1 ~(wr_en & wr_addr==tmp_addr)[*2]，時(shí)間點(diǎn)已經(jīng)來到了120ns；如果前置算子的條件滿足了，那么我們只需要在120ns當(dāng)拍檢查回讀數(shù)據(jù)rd_data==tmp_data是否成功就可以了，這個(gè)斷言是必須要滿足的。

property assert_chk;
    reg [31:0] tmp_data;
    reg [31:0] tmp_addr;
    @(posedge clk) disable iff(~rst_n)
        (rd_en, tmp_addr=rd_addr) ##1 (wr_en & wr_addr==tmp_addr, tmp_data=wr_data) ##1 ~(wr_en & wr_addr==tmp_addr)[*2] |-> rd_data==tmp_data;
endproperty

3.什么時(shí)候我們需要對(duì)第2拍繼續(xù)hazard呢？條件就是第2拍有對(duì)同一地址的寫入（顯然第0、1拍有沒有已經(jīng)不重要了），且之后的1拍沒有同一地址的寫入，那么讀回?cái)?shù)據(jù)必須是第1拍寫入的數(shù)據(jù)，波形示意如下：

不多分析了，直接寫：

property assert_chk;
    reg [31:0] tmp_data;
    reg [31:0] tmp_addr;
    @(posedge clk) disable iff(~rst_n)
        (rd_en, tmp_addr=rd_addr) ##2 (wr_en & wr_addr==tmp_addr, tmp_data=wr_data) ##1 ~(wr_en & wr_addr==tmp_addr)[*1] |-> rd_data==tmp_data;
endproperty

4.什么時(shí)候我們需要對(duì)第3拍繼續(xù)hazard呢？條件就是第3拍有對(duì)同一地址的寫入（不需要任何其他條件了）讀回?cái)?shù)據(jù)必須是第3拍寫入的數(shù)據(jù)，波形示意如下：

那么可以直接寫出斷言了：

property assert_chk;
    reg [31:0] tmp_data;
    reg [31:0] tmp_addr;
    @(posedge clk) disable iff(~rst_n)
        (rd_en, tmp_addr=rd_addr) ##3 (wr_en & wr_addr==tmp_addr, tmp_data=wr_data) |-> rd_data==tmp_data;
endproperty

我們觀察了一下，這個(gè)形式跟之前的好像有點(diǎn)不太和諧，沒關(guān)系可以修理一下，這里我們使用一個(gè)特殊重復(fù)算子[*0]，他的作用是什么呢？是向前吃掉一拍的操作，舉幾個(gè)例子感受下：

• req_a ##N req_b[*0] 等價(jià)于req_a ##N-1 req_b；

• req_a ##1 req_b[*0] 等價(jià)于req_a；

• req_a[*0] ##N req_b 等價(jià)于 ##N-1 req_b；

• req_a[*0] ##1 req_b 等價(jià)于 req_b；

通過這個(gè)特殊算子，我們可以改寫如下（[*0]吃掉了##1 ~(wr_en & wr_addr==tmp_addr)）：

property assert_chk;
    reg [31:0] tmp_data;
    reg [31:0] tmp_addr;
    @(posedge clk) disable iff(~rst_n)
        (rd_en, tmp_addr=rd_addr) ##3 (wr_en & wr_addr==tmp_addr, tmp_data=wr_data) ##1 ~(wr_en & wr_addr==tmp_addr)[*0] |-> rd_data==tmp_data;
endproperty

好的，四種情景我們已經(jīng)寫好了，下面把他們放在一起來觀察下，仿佛規(guī)律套路很深?。∮^察了一個(gè)小時(shí)后我們發(fā)現(xiàn)，里面除了數(shù)字不一樣其他的根本就是完全一樣的。

property assert_chk;
    reg [31:0] tmp_data;
    reg [31:0] tmp_addr;
    @(posedge clk) disable iff(~rst_n)
        (rd_en, tmp_addr=rd_addr) ##0 (wr_en & wr_addr==tmp_addr, tmp_data=wr_data) ##1 ~(wr_en & wr_addr==tmp_addr)[*3] |-> rd_data==tmp_data;
endproperty

property assert_chk;
    reg [31:0] tmp_data;
    reg [31:0] tmp_addr;
    @(posedge clk) disable iff(~rst_n)
        (rd_en, tmp_addr=rd_addr) ##1 (wr_en & wr_addr==tmp_addr, tmp_data=wr_data) ##1 ~(wr_en & wr_addr==tmp_addr)[*2] |-> rd_data==tmp_data;
endproperty

property assert_chk;
    reg [31:0] tmp_data;
    reg [31:0] tmp_addr;
    @(posedge clk) disable iff(~rst_n)
        (rd_en, tmp_addr=rd_addr) ##2 (wr_en & wr_addr==tmp_addr, tmp_data=wr_data) ##1 ~(wr_en & wr_addr==tmp_addr)[*1] |-> rd_data==tmp_data;
endproperty

property assert_chk;
    reg [31:0] tmp_data;
    reg [31:0] tmp_addr;
    @(posedge clk) disable iff(~rst_n)
        (rd_en, tmp_addr=rd_addr) ##3 (wr_en & wr_addr==tmp_addr, tmp_data=wr_data) ##1 ~(wr_en & wr_addr==tmp_addr)[*0] |-> rd_data==tmp_data;
endproperty

那么就試著把他們合到一起吧，合到一起是什么樣子呢？

property assert_chk;
    reg [31:0] tmp_data;
    reg [31:0] tmp_addr;
    @(posedge clk) disable iff(~rst_n)
        (rd_en, tmp_addr=rd_addr) ##0
        ((##[0:3] wr_en & wr_addr==tmp_addr, tmp_data=wr_data) ##1 ~(wr_en & wr_addr==tmp_addr)[*0:3])) |-> rd_data==tmp_data;
endproperty

就是這樣對(duì)不對(duì)？！可是我們觀察下上面這個(gè)斷言是有明顯問題的，我們希望的是當(dāng)前面取##0后面取[*3]，前面取##1后面取[*2]，前面取##2后面取[*1]，前面取##3后面取[*0]對(duì)吧！那么我們要怎么辦呢？是時(shí)候再把最好用的intersect拿出來了，記得intersect的作用吧，必須前后的序列等長才會(huì)匹配成功，我們想下前面取##0后面取[*3]這個(gè)序列長度是多少呢？是4拍長度對(duì)吧(別忘了里面還插著要給##1呢哈)；以此類推，是不是每種匹配的情況都是4拍長度！所以我們只要約束((##[0:3] wr_en & wr_addr==tmp_addr, tmp_data=wr_data) ##1 ~(wr_en & wr_addr==tmp_addr)[*0:3]))這個(gè)事在4拍內(nèi)匹配就行了呀，怎么約束呢？使用intersect ##3 1‘b1，注意真的不是##4，看一下下面的波形就更清楚了，60ns再##3 1‘b1是在什么時(shí)候匹配的，是不是在120ns處！所以這樣一約束，就使得intersect之前的序列在4拍之內(nèi)匹配成功才會(huì)觸發(fā)斷言的|->檢查了。

這個(gè)技巧真的很好用，望掌握（話說回來，這個(gè)看不懂也沒關(guān)系，太難了我覺得）。

答案

property assert_chk;
    reg [31:0] tmp_data;
    reg [31:0] tmp_addr;
    @(posedge clk) disable iff(~rst_n)
        ((rd_en, tmp_addr=rd_addr) ##0
        (((##[0:3] wr_en & wr_addr==tmp_addr, tmp_data=wr_data) ##1 ~(wr_en & wr_addr==tmp_addr)[*0:3])) intersect ##3 1'b1) |-> rd_data==tmp_data;
endproperty

驗(yàn)證

錯(cuò)誤的情況：

"/home/ICer/test.sv", 510: testbench.u_test.assert_test: started at 365000ps failed at 395000ps
Offending '(rd_data == tmp_data)'
$finish called from file "../top/testbench.sv", line 35.

正確的情況：

好了，飛不飛升我不知道，反正我人要沒了。