前言

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

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

練習1

題目

系統復位后，狀態機信號status在任意一拍均有且只有1bit信號有效。

分析

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

答案

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

驗證

注意嗷，對于onehot函數，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.

練習2

題目

系統復位后，data信號在任何時刻均不能為X態或Z態。

分析

和上一個題目類似，可以直接調用系統函數，注意是不能為X態或Z態。

答案

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

太簡單了，就不進行仿真確認了哈。

練習3

題目

某一奇怪的握手協議中規定，vld信號只能在ready信號有效期間有效。

分析

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

答案

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

練習4

題目

接口data_vld有效時，data信號值必須處于合理的范圍內（假設合理范圍時‘h0000~'h7FFF）。

分析

data信號值處于合理范圍需要用到inside方法，他本身就是檢查一個值是否處于之后的范圍內。

答案

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

驗證

"/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.

練習5

題目

data_vld是一個檢測上升沿的單拍脈沖信號，最多有效1拍就會拉低等待下次觸發。

分析

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

答案

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

練習6

題目

單比特信號data_vld連續有效時間跨度最多為5拍。

分析

要檢查vld信號每次為1應該持續[1:5]拍，想想什么操作符是連續持續n拍呢？a[*n]：連續重復運算符，a[*2:4]含義為a信號重復2~4拍。不如我們先寫一個簡單的，如果規定vld有效必須為5拍，那么我們怎么寫呢？這里肯定要用到$rose和$fell函數了，因為持續幾拍肯定是從頭數到尾我們需要上升沿和下降沿；持續幾拍那就用到了我們連續重復了[*m:n]，那我們先寫一個看看：

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

看上去挺合理的，data_vld有效開始檢查，到data_vld無效時結束，在這期間data_vld連續有效了5拍，如果不是5拍就報錯。不過這樣寫是有問題的，問題請見下面的波形，這很明顯是一個維持了5拍的信號對吧：

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

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

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，完美的解決了這個問題，這個用法一定要牢記。

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

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

答案

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

驗證

data_vld分別持續了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.

練習7

題目

req信號（單拍脈沖）有效之后（含當拍），rsp信號有效之前（含當拍），必須要收到（出現）4次data_vld有效。

分析

這個題目和上一個題有點類似，我們來分析一下。這個斷言應該在req有效當拍開始而在rsp有效（第一次有效）時結束，我們關注的就是req->rsp之間的事情。所以很顯然前置算子就是req（因為是單拍信號，所以不需要用$rose）。后面怎么寫呢？我們可以使用intersect + [->1]的句式，a [->n]：非連續跟隨重復符，或者叫go-to重復符，含義是a非連續(就是無所謂連不連續)重復n次，只在第n次重復時刻點匹配（跟隨的含義）。最常用的a [->1]等價于(!a) [*0:$] ##1 a，也就是匹配了a序列第一次成立的時刻。

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

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

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

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

答案

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

驗證

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

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.

練習8

題目

req信號（單拍脈沖）有效之后（不含當拍從下一拍開始），rsp信號有效之前（不含當拍，rsp有效之前），必須要收到（出現）4次data_vld有效。

分析

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

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

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

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

再看一個略帶迷惑性的例子，如下圖這個行為最后斷言是會報成功還是失敗呢？我和同學有一些爭論，不過我認為是會成功的，因為在220ns時（data_vld[=4] ##1 1'b1）報匹配成功，rsp[->1]在220ns處報匹配成功，intersect前后序列等長斷言匹配成功，檢查也就此結束。不過你說在220ns處data_vld[=5]了，那沒關系因為（data_vld[=5] ##1 1'b1）作為一個整體在240ns才匹配此時我的斷言都已經檢查完成了，等待下一次req有效才會開始下一次檢查，因此對斷言成功沒有影響。

答案

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

驗證

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

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.

練習9

題目

上一個題的變種，稍有變化。n_ready是維持信號，在n_ready有效期間，data_vld信號有效的次數應該小于等于4次，data_vld信號為離散信號。

分析

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

注意n_ready是維持信號，因此我們選取前置算子時候要選取的是n_ready的上升沿$rose(n_ready)；我們仍舊選擇intersect+[->1]的組織形式，那么后面跟的應該是!n_ready[->1]即檢查結束點為n_ready無效的時刻，因此也可以寫成$fell(n_ready)[->1]，[->1]這個意思就是第一次成功的意思哈。初步組織斷言為：

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

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

要避免這一個問題還是要用到上個練習的方法，引入##1 1'b1（還是直接理解成把序列匹配的時間點往后推一拍），這樣在220ns處(data_vld[0:4] ##1 1'b1)處于匹配成功的時間點，整個斷言判定成功。220ns處的data_vld就被這個##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

驗證

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.

練習10

題目

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

分析

這其實也是系統中比較常見的一個場景，那么我們來組織一下斷言；從前置算子入手，因為說了req是單拍脈沖信號所以前置算子可以直接寫req了；后面要斷的是什么呢？是在rsp[->1]之前req不能為1，所以可以使用intersect (rsp[->1])句式，寫成~req intersect (rsp[->1])；我們觀察下intersect前面是一個信號表達式，那么就跟前面我寫的東西連上了，這里也可以用throughout來連接等長的表達式與序列；而要使用|->還是|=>來連接呢？必須使用|=>來連接的，因為你從不能在req有效的當拍斷言檢查req無效吧？

答案

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

驗證

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.

練習11

題目

某個模塊接收前級模塊發送的請求req，請求以req_id作為標記，本模塊以rep和rep_id作為響應信號表示已經接收到請求；請檢查req和req_id有效后，最近的一拍rsp有效時rsp_id等于req_id。

分析

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

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

答案

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

驗證

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.

練習12

題目

某個模塊接收前級模塊發送的請求req，請求以req_id作為標記，本模塊以rep和rep_id作為響應信號表示已經接收到請求；請檢查req有效后，下一次req有效時req_id為上一次req_id加1（0~FF~0循環發送id）。

分析

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

答案

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

練習13

題目

某個模塊接收前級模塊發送的請求req，請求以req_id作為標記，本模塊以rep和rep_id作為響應信號表示已經接收到請求；某個id被本模塊相應前，不應該再收到相同id的req請求。

分析

不用分析，使用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

驗證

4'hB的req還沒回，又發過來一個同樣id的請求，報錯了。

"/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.

練習14

題目

某模塊與兩個前級模塊對接，前級模塊1發送請求req1和req1_id，前級模塊2發送請求req2和req2_id，當該模塊在同一拍收到兩個前級模塊的請求且req_id一致時，需要保證首先對前級模塊1進行響應。

分析

直接解答吧。

答案

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

驗證

"/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.

練習15

題目

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

分析

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

1.什么時候我們需要對第0拍繼續hazard呢？條件就是第0拍有對同一地址的寫入，且之后的3拍沒有同一地址的寫入，那么讀回數據必須是第0拍寫入的數據，波形示意如下：

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

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.什么時候我們需要對第1拍繼續hazard呢？條件就是第1拍有對同一地址的寫入（顯然第0拍有沒有已經不重要了或者說不必關心了），且之后的2拍沒有同一地址的寫入，那么讀回數據必須是第1拍寫入的數據，波形示意如下：

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

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.什么時候我們需要對第2拍繼續hazard呢？條件就是第2拍有對同一地址的寫入（顯然第0、1拍有沒有已經不重要了），且之后的1拍沒有同一地址的寫入，那么讀回數據必須是第1拍寫入的數據，波形示意如下：

不多分析了，直接寫：

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.什么時候我們需要對第3拍繼續hazard呢？條件就是第3拍有對同一地址的寫入（不需要任何其他條件了）讀回數據必須是第3拍寫入的數據，波形示意如下：

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

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

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

• req_a ##N req_b[*0] 等價于req_a ##N-1 req_b；

• req_a ##1 req_b[*0] 等價于req_a；

• req_a[*0] ##N req_b 等價于 ##N-1 req_b；

• req_a[*0] ##1 req_b 等價于 req_b；

通過這個特殊算子，我們可以改寫如下（[*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

好的，四種情景我們已經寫好了，下面把他們放在一起來觀察下，仿佛規律套路很深啊！觀察了一個小時后我們發現，里面除了數字不一樣其他的根本就是完全一樣的。

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

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

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

答案

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

驗證

錯誤的情況：

"/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.

正確的情況：

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