[SVA]SystemVerilog Assertion常用操作符总结及案例_intersect sva

SystemVerilog Assertion常用操作符总结及案例

       前言：在数字电路验证中，常常需要对某一组信号之间的关系做检查，此时就要用到SystemVerilog Assertion。用过能掌握SVA的一些语法，将大大减小了check的代码量。针对信号持续重复的情况，SVA提供了三种重复操作符：Consecutive repetition（持续性重复），go to repetition(跟随重复操作）和non-consecutive repetition（非连续重复操作）。本文将分别介绍这三种操作符的含义及使用方法。

一、持续重复操作（Consecutive repetition）

 1.1 信号的重复

• 原语： signal or sequence [*n] 其中n为重复的次数
• 含义：持续性重复允许指定x信号或序列持续性匹配指定周期数，重复周期之间默认有一时钟周期的间隔。

(a##1b)[*3];                 //等价于 a##1b##1a##1b##1a##1b

• 示例（1）信号的重复：start上升沿两个时钟周期后，a持续为高3个时钟周期，再经过两个时钟周期后，stop拉高1个时钟周期

property p21;
  @(posedge clk);
  $rose(start)|->##2 (a[*3]) ##2 stop ##1 !stop;
endproperty
 
a21: assert property(p21) else $error();

 1.2 带有延迟窗的重复

property p23;
  @(posedge clk) 
  $rose |-> ##2 ((a##[1:4]b)[*3]) ##2 stop;
endproperty
 
a23: assert property(p23) else $error();
//(a##[1:4]b)[*3]等价于：
//((a##1b) or (a##2 b) or (a##3 b) or (a##4b))##1
//((a##1b) or (a##2 b) or (a##3 b) or (a##4b))##1
//((a##1b) or (a##2 b) or (a##3 b) or (a##4b))

 1.3 带有不确定性的持续性重复

• 含义：持续性重复可以指定秩序性重复的最小和最大次数，信号持续性重复次数在这个范围内都匹配正确。其重复次数上限可以设为$表示无穷.
• 示例：a[*1:5]等价于a or (a##1a) or (a##1 a ##1 a) or (a##1 a##1 a##1 a )or (a##1 a##1 a##1 a##1 a)

property p24;
  @(posedge clk)
  $rose(start) |-> ##2 (a[*1:$]) ##1 stop;
endproperty
 
a24: assert property(p24) else $error();

二、跟随重复操作（go to repetition）

 2.1 不要求信号持续重复，可以是间断性的，但要求最后一次匹配必须在序列匹配的最后一个时钟周期。

• 原语：Sigbnal [->n]
• 含义：Start ##1 a[->3] ##1 stop;  //要求a重复三次且必须最后一次出现紧接着stop信号。
• 示例：p25要求a最后一次出现必须紧接着stop信号。

property p25;
  @(posedge clk) 
  $rose(start) |->##2 (a[->3]) ##1 stop;
endproperty
 
a25:assert property(p25) else $error();

三、非连续重复操作（non-consecutive repetition）

 3.1 非持续性重复操作不要求信号连续重复，也不要求信号最后一次匹配必须在序列的最后一个时钟周期。

• 原语：Signal [=n]
• 示例：p26中序列要求检测到start上升沿后两个时钟周期后，a应重复3次，但不要求持续重复，随后再过一个时钟周期，stop拉高一个时钟周期。

property p26;
  @(posedge clk) 
  $rose(start) |->##2 (a[=3]) ##1 stop ##1 !stop;
endproperty
 
a26:assert property(p26) else $error();  

• 注意，start上升沿后两个时钟周期后不要求a立即为高，只需要确保在start上升沿于stop拉高之间有三个a高电平即可，跟随重复操作类似。
• 案例：check如下sequence：在信号a为高期间，信号b会出现1个posedge，但是信号b出现posedge时，信号a不一定为高电平 

property b_posedge();
  @(posedge clk_ck) disable iff(~rst_n)
  $rose(a) |-> ($rose(b)[1]) ##1 $fell(a);
endproperty

 3.2 区别与联系

• [->n]只有给操作符后边跟其他表达式才可以看出两者的区别。
• 满足[->n]必定满足[=n]，满足[*n]必定满足[->n]和[=n]。

四、其他操作符

 4.1 同步操作符intersect

• 含义：操作符intersect为and操作符特例，它要求两个序列同时开始，同时结束。换句话说，就是要求两个序列的长度必须相等。
• 示例：p28相当于要求s28a和s28b要有相同的长度序列。

sequence s28a;
    @(posedge clk) a##[1:2] b;
endsequence
 
sequence s28b;
    @(posedge clk) c##[2:3] d;
endsequence
 
property p28;
   @(posedge clk) s28a intersect s28b;
endproperty
 
a28:assert property(p28) else $error();

• 应用：intersect也可用于控制序列的长度，用于限定那些未设定窗口上限的序列定义检测时长
• 示例：p35中由于intersect的使用，序列应在三至五个时钟周期内检查完毕，否则断言失败。

property p35;
    @(posedge clk) 1[*3:5] intersect(a##[1:$] b ##[1:$] c));
endproperty
 
a35:assert property(p35) else $error();

 4.2 first_match操作

• 含义：针对带有时序窗口的序列，同一起始点可能有多个匹配到的序列，fisrt_match用于确保只用第一次匹配成功的序列而丢弃其他匹配的序列，用于针对同一个校验具有多个匹配的情况。
• 示例：对于p30来讲，对于每个起始点都有5中可能匹配的序列，first_match在得到一个成功匹配的点后，其他情况将不会再考虑匹配。

sequence s30a;
 @(posedge clk) a##[1:3] b;
endsequence
 
sequence s30b;
 @(posedge clk) c##[2:3]d;
endsequence
 
property p30;
 @(posedge clk) first_match(s30a or s30b);
endporperty
 
a32:assert property(p30) else $error();

 4.3 throughout操作符

• 含义：throughout操作符用于保证某些条件在整个序列的验证过程中一直为真。
• 原语：（expression）throughout （sequence definition）
• 在整个sequence definition验证期间，expression表达式必须一直保持为真。
• 即使验证序列匹配成功但表达式不为真，也会导致整个验证序列的验证失败。
• 示例：p31要求在序列检查期间，start信号必须保持为低电平

property p31;
  @(posedge clk)
  $fell(start) |-> (!start) throughout (##1 (!a&&!b) ##1 (c[->3]) ##1 (a&&b));
endproperty
 
a31:assert property(p31) else $error();

 4.4  within操作符

• 原语：seq1 within seq2
• 含义：with原语规定seq1在seq2的开始到结束范围内发生，即seq2的开始匹配点必须不晚于seq1的开始匹配点，seq2的匹配结束点必须不晚于seq1的结束匹配点。

sequence s32a;
  @(posedge clk)
  ((!a&&!b) ##1 (c[->3]) ##1 (a##b));
endsequence
 
sequence s32b;
 @(posedge clk)
 $fell(start) ##[5:10] $rose(start);
endsequence
 
sequence s32;
  @(posedge clk) s32a within s32b;
endsequence
 
property p32;
  @(posedge clk) $fell(start)|->s32;
endproperty
 
a32:assert property(p32) else $error();

 4.5  matched

• 任何时候如果一个序列定义了多个时钟，构造“matched”可以用来监测第一
  个子序列的结束点。

sequence s_a; 
  @(posedge clk1) $rose(a); 
endsequence 
 
sequence s_b; 
  @(posedge clk2) $rose(b); 
endsequence 
 
property p_match; 
  @(posedge clk2) s_a.matched |=> s_b; 
endproperty 
 
a_match： assert property(p_match); 

 

五、if/else结构使用

• SVA也允许在属性property中使用if/else结构
• 示例：a取不同值时，进行不同的check

property p_if_else;
    @(posedge clk) ($fell(start) ##1 (a||b)) |->
      if(a)
         (c[->2] ##1 e);
      else
         (d[->2] ##1 f);
endproperty
 
a_if_else:assert: property(p_if_else) else $error();

六、expect操作符

• 含义：expect操作符类似于verilog中的wait。
• 作用：expect用于等待一个成功检测的property，并带有阻塞作用。
• 原语：expect的原语结构非常类似于assert，并允许带有成功与失败情况下的响应块儿（else ...）。
• 示例：当cpu_ready被置位后，expect期待在1至16个时钟周期内memory_ready被置位。若memory_ready如期被置位，执行for循环，否则报错并退出。

initial begin
    @(posedge clk);
    #2ns cpu_ready=1'b1;
    expect(@(posedge clk) ##[1:16] memory_ready =='b1)
       $dispaly("Hand shake successful\n");
    else begin
        $display("Hand shake failed:exiting");
        $finish();
    end
    for(i=0;i<64;i++) begin
         ...
    end
end

七、局部变量的使用

• SVA允许在property和sequence中声明局部变量。局部变量在使用时紧跟子序列，用逗号隔开。
• 当子序列成功匹配时，变量赋值被执行。每次序列执行时，变量均会创建一个副本。
• 示例：p_local_var1中$rose(enable1)匹配成功才会对lvar1赋值。

property p_local_var1;
    int lvar1;
    @(posedge clk)
    ($rose(enable1),lvar1=a) |-> ##4 （aa==(lvar1*lvar1*lvar1)）;
endproperty
 
a_local_var1: assert property(p_local_var1) else $error();

八、逻辑操作符

 8.1 and

• 逻辑操作符and用于组合两个序列，当所有的序列都成功匹配后才通过检测。所有的序列在同一时间开始但可以在不同时间结束。

sequence s27a;
    a##[1：2] b;
endsequece
 
sequence s27b;
    c##[2:3] d;
endsequence
 
property p27;
   @(posedge clk) s27a and s27b;
endproperty
 
a27:assert property(p27) else $error();

 8.2 or

• 逻辑操作符or当序列中的其中一个验证成功后即匹配成功。

sequence s29a;
   @(posedge clk) a##[1:2] b;
endsequence
 
sequence s29b;
  @（posedge clk）c##[2:3]d;
endsequence
 
property p29;
  @(posedge clk) s29a or s29b;
endproperty
 
a29: assert property(p29) else $error();