sva_assertion: 15道助力飞升的断言练习

前言

纸上得来终觉浅，绝知此事要躬行。把之前学习到的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.

正确的情况：

好了，飞不飞升我不知道，反正我人要没了。