SVA中的序列表达式操作符

在SVA中构造一些比较复杂的序列时，常用的交叠操作符有时已经不能满足要求，为此在SVA中引入了一些可以用于构造特定要求序列的表达式操作符：intersect、within、throughout、first_match、ended、matched等。下面将示例这些特殊的操作实现的功能。

1 intersect

intersect两侧的表达式都是sequence，不能是property，使用intersect时需要确保其两侧的sequence必须同时开始，且当两个sequence最终同时匹配时才认为两个序列的intersect匹配，即两个sequence匹配的长度必须相同，intersect操作符和and操作符很相似，但是and没有要求两个序列最终匹配时同时匹配。intersect使用示意图如下：

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2,sig3,sig4;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
       sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;
       sig3 = 1'b0;sig4 = 1'b0;
    #4 sig0 = 1'b1;
    #2 sig0 = 1'b0;sig1 = 1'b1;sig3 = 1'b1;
    #2 sig3 = 1'b0;sig1 = 1'b0;sig2 = 1'b1;
    #2 sig3 = 1'b0;
    #2 sig2 = 1'b1;sig4 = 1'b1;
    #2 sig2 = 1'b0;sig4 = 1'b0;
    #2 $stop;
end

sequence s1;
    sig1 ##[1:5] sig2;
endsequence  // s1
sequence s2;
    sig3 ##[2:4] sig4;
endsequence  // s2

property p;
    @(posedge clk) $rose(sig0) |-> ##1 (s1 intersect s2);
endproperty // p
property p1;
    @(posedge clk) $rose(sig0) |-> ##1 s1;
endproperty // p1
property p2;
    @(posedge clk) $rose(sig0) |-> ##1 s2;
endproperty // p2

a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);
a1 : assert property(p1) $display("@%0t | p1 : PASSED!",$time);
     else $display("@%0t | p1 : FAILED!",$time);
a2 : assert property(p2) $display("@%0t | p2 : PASSED!",$time);
     else $display("@%0t | p2 : FAILED!",$time);
endmodule // top_tb

【仿真结果】

示例的仿真结果中，序列s1在9ns处匹配，序列s2在13ns处匹配，表面看起来两者匹配的结束点不一样，但是s1实际上在9ns、11ns、13ns处均有匹配点，只是属性p1中，因为s1之后没有其他的表达式，所以s1按照“左侧就近匹配原则”进行了匹配，所以出现了仿真结果中a1情况。s1和s2在intersect进行分析匹配时，会将两个序列的所有匹配点进行分析，当这些匹配点处存在第一次同时匹配时即认为“s1 intersect s2”匹配成功，如果没有同时匹配，则认为“s1 intersect s2”匹配不成功。

2 within

within右侧sequence的起止点必须位于左侧sequence的起止点之内，当然within左右两侧sequence的起止点可以一样，整个“sequence_1 within sequence_2”匹配成功的结束点与右侧sequence的结束点一致。within使用示意图如下：

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2,sig3,sig4;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
       sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;
       sig3 = 1'b0;sig4 = 1'b0;
    #4 sig0 = 1'b1;
    #2 sig0 = 1'b0;sig1 = 1'b1;
    #2 sig1 = 1'b0;
    #2 sig3 = 1'b1;
    #2 sig3 = 1'b0;
    #4 sig4 = 1'b1;
    #2 sig4 = 1'b0;sig2 = 1'b1;
    #2 sig2 = 1'b0;
    #2 $stop;
end

sequence s1;
    sig1 ##[1:6] sig2;
endsequence  // s1
sequence s2;
    sig3 ##[3:4] sig4;
endsequence // s2

property p;
    @(posedge clk) $rose(sig0) |-> ##1 (s2 within s1);
endproperty // p
property p1;
    @(posedge clk) $rose(sig0) |-> ##1 s1;
endproperty // p1
property p2;
    @(posedge clk) $rose(sig0) |-> ##3 s2;
endproperty // p2
a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);
a1 : assert property(p1) $display("@%0t | p1 : PASSED!",$time);
     else $display("@%0t | p1 : FAILED!",$time);
a2 : assert property(p2) $display("@%0t | p2 : PASSED!",$time);
     else $display("@%0t | p2 : FAILED!",$time);        
endmodule // top_tb

【仿真结果】

序列s2“sig3 ##[3:4] sig4”的起止点位于序列s1“sig1 ##[1:6] sig2”起止点之内，整个属性p的最终匹配点与序列s1相同，即“sequence_1 within sequence_2”匹配的起止点取决于其中最长的那个sequence。

3 throughout

在SVA中有时需要某些信号在一个序列的检查过程中一直保持一个状态，此时就可以使用throughout操作符，当这些信号的状态发生不期望的变化时，序列的检查即认为失败。throughout使用示意图如下：

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2,sig3;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
       sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;sig3 = 1'b0;
    #2 sig0 = 1'b1;
    #2 sig0 = 1'b0;sig1 = 1'b1;sig2 = 1'b1;
    #2 sig2 = 1'b0;
    #6 sig3 = 1'b1;
    #2 sig3 = 1'b0;sig1 = 1'b0;
    #4 sig0 = 1'b1;
    #2 sig0 = 1'b0;sig1 = 1'b1;sig2 = 1'b1;
    #2 sig2 = 1'b0;
    #2 sig1 = 1'b0;
    #2 sig1 = 1'b1;
    #2 sig3 = 1'b1;
    #2 sig3 = 1'b0;sig1 = 1'b0;
    #2 $stop;
end

sequence s;
    sig2 ##[1:6] sig3;
endsequence  // s

property p;
    @(posedge clk) $rose(sig0) |-> ##1 (sig1 throughout s);
endproperty // p

a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);    
endmodule // top_tb

【仿真结果】

示例中，当sig1在序列s“sig2 ##[1:6] sig3”检查过程中保持稳定的状态，并且伴随序列s正常匹配结束，即认为“sig1 throughout s”匹配成功。如果sig1在序列s“sig2 ##[1:6] sig3”检查过程中发生变化，发生不期望变化的地方即是“sig1 throughout s”匹配失败之处，如仿真中25ns处。

这里需要注意，在SVA中还存在着另一种操作符“disable iff”其功能与throughout非常类似，但是在使用时还需要注意两者的差异。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk,rst;
logic sig0,sig1,sig2,sig3;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
       sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;sig3 = 1'b0;rst = 1'b0;
    #2 rst  = 1'b1;
    #2 sig0 = 1'b1;
    #2 sig0 = 1'b0;sig1 = 1'b1;sig2 = 1'b1;
    #2 sig2 = 1'b0;
    #6 sig3 = 1'b1;
    #2 sig3 = 1'b0;sig1 = 1'b0;
    #4 sig0 = 1'b1;
    #2 sig0 = 1'b0;sig1 = 1'b1;sig2 = 1'b1;
    #2 sig2 = 1'b0;rst  = 1'b0;
    #2 sig1 = 1'b0;
    #2 sig1 = 1'b1;
    #2 sig3 = 1'b1;
    #2 sig3 = 1'b0;sig1 = 1'b0;
    #2 $stop;
end

sequence s;
    sig2 ##[1:6] sig3;
endsequence  // s

property p;
    @(posedge clk) $rose(sig0) |-> ##1 (sig1 throughout s);
endproperty // p
property pr;
    disable iff(!rst)
    @(posedge clk) $rose(sig0) |-> ##1 (sig1 throughout s);
endproperty // pr

a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);    
a0 : assert property(pr) $display("@%0t | pr : PASSED!",$time);
     else $display("@%0t | pr : FAILED!",$time); 
endmodule // top_tb

【仿真结果】

示例中，通过属性p可以看到，p中throughout两侧序列和相关信号的采样都是基于采样事件的，throughout的作用范围限于其两侧序列和信号的被检查时间。Pr中的disable iff作用时间与当前属性的时间相同，并且当其中条件满足时后续的检查将会被终止并产生空成功（vacuous success），如图中24ns处所示。而且disable iff中的信号不像throughout两侧的表达式是基于采样事件的，disable iff信号可以异步于采样事件存在。由此可见，disable iff和throughout区别可总结如下：

disable iff	throughout
作用时间等同于当前property	作用时间为其两侧序列和信号被检查的时间
可以异步于当前采样事件	与当前采样事件同步
如果iff后的条件发生，将终止当前序列表达式的检查，产生空成功	如果其两侧的序列或者信号不匹配，那么当前序列会失败

4 first_match

在对一些指定时序窗口同时发生的多个序列进行检查时，使用first_match可以检查这些同时发出的序列进程中第一个完成匹配的序列，然后丢弃对于其他未完成序列进程的检查。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2,sig3;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
       sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;sig3 = 1'b0;
    #2 sig0 = 1'b1;sig1 = 1'b1;
    #2 sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b1;
    #6 sig2 = 1'b0;
    #2 sig3 = 1'b1;
    #2 sig3 = 1'b0;
    #2 $stop;
end

property p1;
    @(posedge clk) $rose(sig0) |-> sig1 ##1 sig2[*1:4] ##2 sig3;
endproperty // p1
property p2;
    @(posedge clk) $rose(sig0) |-> sig1 ##1 first_match(sig2[*1:4]) ##2 sig3;
endproperty // p2

a1 : assert property(p1) $display("@%0t | p1 : PASSED!",$time);
     else $display("@%0t | p1 : FAILED!",$time);    
a2 : assert property(p2) $display("@%0t | p2 : PASSED!",$time);
     else $display("@%0t | p2 : FAILED!",$time); 
endmodule // top_tb

【仿真结果】

示例中对应sig2[*1:4]会同时开启4个并行的进程，分别检查sig2连续匹配1次、2次、3次和4次为高的情况，四个进程只要有一个匹配成功即认为sig2[*1:4]匹配成功一次。p1中在sig2[*1:4]三次匹配后两个采样周期检测到sig3为高，即认为当前属性断言成功，其实sig2[*1:4]第三次匹配前已经完成了两次匹配，只是前两次匹配后的两个采样周期并没有检测到sig3为高，所以被舍弃，而sig2[*1:4]第三次匹配成功后的两个采样周期sig3也匹配，所以sig2[*1:4]第四次检查被舍弃。p2中“first_match(sig2[*1:4])”将仅使用“sig2[*1:4]”开启的4个并行进程中第一次匹配的进程，示例中，“sig2[*1:4]”在5ns处第一次匹配后检测其后两个采样周期sig3是不是匹配，结果sig3不为高即不匹配，所以此时属性p2断言失败，而后续其他几次还在进行中的进程将会被舍弃。可见first_match可以确保第一序列的匹配，而丢弃后续还未完成的其他正在进行的序列。

5 ended

详见“SVA中被抛弃的ended”

6 matched

在一些场景，可能会碰到这样的情况：在一个属性中不同序列基于不同的采样事件，那么如何在基于不同采样事件的序列之间进行交互呢？在SVA中使用matched可以用来检测其中一个子序列的结束点，从而实现基于不同采样事件的序列之间的同步交互。与ended结构类似，使用matched的序列必须要有自己的采样事件，不同的是matched序列使用的采样事件可以与调用其的属性使用的采样事件不同。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk1,clk2;
logic sig1,sig2;

initial begin
    clk1 = 1'b0;clk2 = 1'b0;
    fork 
        forever #1 clk1 = ~clk1;
        forever #2 clk2 = ~clk2;
    join
end

initial begin
       sig1 = 1'b0;sig2 = 1'b0;
    #2 sig1 = 1'b1;
    #2 sig1 = 1'b0;
    #2 sig2 = 1'b1;
    #4 sig2 = 1'b0;
    #2 sig1 = 1'b1;
    #2 sig1 = 1'b0;
    #2 sig2 = 1'b1;
    #4 $stop;
end

sequence s1;
    @(posedge clk1) $rose(sig1);
endsequence // s1
sequence s2;
    @(posedge clk2) $rose(sig2);
endsequence // s2

property p;
    @(posedge clk2) s1.matched |-> ##1 s2;
endproperty // p

a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time); 
endmodule // top_tb

【仿真结果】

s1基于采样事件clk匹配后，s1.matched的结果会暂存起来，在经过一个clk2采样事件后基于采样事件clk2的s2匹配，此时整个属性完成匹配。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk1,clk2;
logic sig0,sig1,sig2;

initial begin
    clk1 = 1'b0;clk2 = 1'b0;
    fork 
        forever #1 clk1 = ~clk1;
        forever #2 clk2 = ~clk2;
    join
end

initial begin
       sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b1;
    #4 sig1 = 1'b1;
    #1 sig0 = 1'b1;
    #1 sig2 = 1'b0;sig1 = 1'b0;
    #8 $stop;
end

sequence s;
    @(posedge clk1) $rose(sig1) ##1 $fell(sig2);
endsequence // s

property p1;
    @(posedge clk2) $rose(sig0) |=> s.matched;
endproperty // p1
property p2;
    @(posedge clk2) $rose(sig0) |=> @(posedge clk1) s.matched;
endproperty // p2

a1 : assert property(p1) $display("@%0t | p1 : PASSED!",$time);
    else $display("@%0t | p1 : FAILED!",$time); 
a2 : assert property(p2) $display("@%0t | p2 : PASSED!",$time);
    else $display("@%0t | p2 : FAILED!",$time); 
endmodule // top_tb

【仿真结果】

示例中，序列s在7ns处匹配成功，s.matched结果将会保存着。$rose(sig0)在6ns时基于clk2匹配成功，即属性p1中“|=>”先行算子$rose(sig0)匹配，但是后续算子在属性p1中并没有明确指定采样事件，所以此处属性的匹配将在基于clk2的先行算子匹配后的一个采样周期

匹配成功。在属性p2中，后续算子指定了采样事件为clk1，此时前后算子基于不同的采样事件，在基于clk2采样事件的先行算子满足要求之后，在距离其最近的基于clk1采样事件的时刻检查s.matched是否匹配，而示例中s.matched在7ns时满足要求，所以此时整个属性匹配成功。这里需要注意，SVA会自动同步不同信号或者子序列使用的时钟域，并且当序列中使用了多个时钟信号时，只允许在其中使用“##1”进行延迟，关于多时钟在SVA中的应用可参考“SVA中的multi-clock”一文。