【握手协议3】握手协议中常用的并发断言介绍¶

同步写在assertion文件中然后bind到module上： 这种方式意味着你将创建一个单独的断言文件，这个文件包含了所有相关的并发断言。然后，你会使用Verilog或SystemVerilog的bind构造将这些断言"绑定"到特定的模块上。这样可以在不修改原本模块代码的情况下增加额外的验证逻辑，使得验证和设计可以分开进行。

写在对应的interface中： 另一种方法是直接在interface定义中包括并发断言。在SystemVerilog中，interface被用来封装与模块间通信相关的信号和协议。在interface内部编写断言意味着这些断言与通信接口紧密关联，可以提高代码的模块化和重用。

而于握手接口对应的interface形式为：

interface axi_ar_interface(input clk, rst_n);

  logic         valid;
  logic         ready;
  logic [8 -1:0]data;

endinterface

那么基于接口命名来完成相关断言。

1.复位后valid不能为不定态（X态或者Z态）

property valid_xz_chk;
    @(posedge clk) disable iff(~rst_n)
        ~$isunkonwn(valid);
endproperty

2.复位后ready不能为不定态（X态或者Z态）

property ready_xz_chk;
    @(posedge clk) disable iff(~rst_n)
        ~$isunkonwn(ready);
endproperty

3.data在valid为1时不能不定态（X态或者Z态）

property data_xz_chk;
    @(posedge clk) disable iff(~rst_n)
        valid |-> ~$isunkonwn(data);
endproperty

4.data在valid为高后，在只有在握手之后才能跳变，否则必须保持

property data_stable_chk;
    @(posedge clk) disable iff(~rst_n)
        valid && !ready |-> ##1 $stable(data);
endproperty

5.valid在valid为高后没有ready握手之前，不能跳变

property valid_stable_chk;
    @(posedge clk) disable iff(~rst_n)
        valid && !ready |-> ##1 valid;
endproperty

6.valid之后若干拍ready必须为1

property data_stable_chk;
    @(posedge clk) disable iff(~rst_n)
        valid |-> ##[0:$] ready;
endproperty