SVA中的基本元素sequence和蕴含操作
1 序列块sequence
序列是断言最基本的组成结构之一，主要描述一些逻辑行为关系，但是在实际的操作过程中该结构也可以省略，当然其存在就有其合理之处，其中一点就是从复用性的角度来说，将可重用的逻辑结构定义于sequence中，然后在property中通过时钟采样触发sequence，这样可以使sequence不依赖于特定的时钟而存在于不同的时钟设计中。当然这并不是说sequence中不能使用时钟等采样事件，只是一般在构建断言时其时钟都是继承于使用调用其的property或者assert的，这个在后续的部分将进行详细的说明。实际中是为了复用性不在其中增加特定时钟而已。另外还需要说明的是property中可以包含sequence，但是sequence中不能包含property，sequence中可以包含其他的sequence。
`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig1,sig2,sig3;
initial begin
clk = 1'b0;
forever #1 clk = ~clk;
end
initial begin
sig1 = 1'b0;sig2 = 1'b0;sig3 = 1'b0;
#2 sig1 = 1'b1;
#2 sig1 = 1'b0;sig2 = 1'b1;
#4 sig3 = 1'b1;
#4 $stop;
end
// sequence
sequence sp;
sig2 ##2 sig3;
endsequence // sp
// property
property pr;
@(posedge clk) sig1 |=> sp;
endproperty // pr
// no sequence in property
property pr1;
@(posedge clk) sig1 |=> sig2 ##2 sig3;
endproperty // pr1
// sequence triggered in property
a1 : assert property(pr) $display("@%0t | a1 : PASSED!",$time);
else $display("@%0t | a1 : FAILED!",$time);
// sequence triggered in assert-property
a2 : assert property(@(posedge clk) sig1 |=>sp) $display("@%0t | a2 : PASSED!",$time);
else $display("@%0t | a2 : FAILED!",$time);
a3 : assert property(pr1) $display("@%0t | a3 : PASSED!",$time);
else $display("@%0t | a3 : FAILED!",$time);
endmodule // top_tb 【仿真结果】 
示例中，sequence和property本身在设计中并不会进行检查，而是需要使用assert property断言他们才会被激活进行相应的检查。sequence不仅可以通过property被assert property触发，也可以直接跳过property直接被assert property触发，但是需要注意的是如果直接在assert property中使用sequence，那么需要在使用的时候指定对应的采样事件（clocking_event），否则将会compile error。如果在property调用sequence时指定了clocking_event，那么在assert property时完全可以不同再次指定clocking_event。可见断言一个序列并不一定要独立的定义一个property，但是如果跳过property直接将sequence加入到assert property中，会造成代码的冗繁不易理解，可重用性和可维护性都很差。所以，出于代码的简单易懂、高可重用性和可维护性建议采用sequence-property-assert property三步式定义和使用。
sequence除了可以被property调用，还可以被其他的sequence调用，其使用格式比较灵活方便。
【示例】
`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 sig1 = 1'b1;sig0 = 1'b0;
#2 sig2 = 1'b1;sig1 = 1'b0;
#2 sig3 = 1'b1;sig2 = 1'b0;
#4 $stop;
end
// base sequence
sequence s0;
sig2 ##1 sig3;
endsequence // s0
// upper sequence
sequence s1;
sig1 ##1 s0;
endsequence // s1
// property
property pr;
@(posedge clk) sig0 |-> ##1 s1;
endproperty // pr
ap : assert property(pr) $display("@%0t | ap : PASSED!",$time);
else $display("@%0t | ap : FAILED!",$time);
endmodule // top_tb 【仿真结果】 
2 蕴含操作
蕴含操作在并行断言中可以说是无处不在，基本上所有的并行断言中都会用到蕴含操作，那么为什么要使用蕴含操作呢？首先先看下面的这个示例。
【示例】
`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1;
initial begin
clk = 1'b0;
forever #1 clk = ~clk;
end
initial begin
sig0 = 1'b0;sig1 = 1'b0;
#2 sig0 = 1'b1;#2 sig0 = 1'b0;
#2 sig1 = 1'b1;#2 sig1 = 1'b0;
#4 $stop;
end
property p;
@(posedge clk) sig0 ##2 sig1;
endproperty // p
a : assert property(p) $display("@%0t | a : PASSED!",$time);
else $display("@%0t | a : FAILED!",$time);
endmodule // top_tb 【仿真结果】 
示例中属性在每个时钟的上升沿都是待检测序列的有效开始，即会在每个时钟周期的上升沿检测sig0是否为高。如果sig0在某个时钟周期的上升沿被采样到不为高，就会产生错误信息，这些信息有时我们并不关心。如果sig0在一段时间内一直保持低，那么将会产生大量的我们不关心的信息，而我们关心的是序列起始点有效后，其后续的序列是否满足要求。示例中，我们关心的是在sig0为高后的第二个时钟周期sig1也为高的情况，如果此时sig1不为高我们才认为序列不匹配。可见在每个采样周期对sig0进行判断后输出信息是不需要的，为了避免冗余的信息，SVA中引入了蕴含操作，当起始序列不满足时将不会输出冗余的不关心的信息，即蕴含操作可以有效的控制时序建模的起点。
【示例】
`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig1,sig2,sig3;
initial begin
clk = 1'b0;
forever #1 clk = ~clk;
end
initial begin
sig1 = 1'b0;sig2 = 1'b0;sig3 = 1'b0;
#2 sig1 = 1'b1;sig3 = 1'b1;
#2 sig1 = 1'b0;sig2 = 1'b1;sig3 = 1'b0;
#2 sig2 = 1'b0; #4 $stop;
end
// sig1在时钟上升沿时为高，在当前时钟上升沿的下一个时钟上升沿时sig2也必须为高
property p1;
@(posedge clk) sig1 |=> sig2;
endproperty // p1
// sig1在时钟上升沿时为高，在当前时钟上升沿sig2也必须为高
property p2;
@(posedge clk) sig1 |-> sig3;
endproperty // p2
a1 : assert property(p1) $display("@%0t | a1 : PASSED!",$time);
else $display("@%0t | a1 : FAILED!",$time);
a2 : assert property(p2) $display("@%0t | a2 : PASSED!",$time);
else $display("@%0t | a2 : FAILED!",$time);
endmodule // top_tb 【仿真结果】
示例中的仿真可以看出，此时的检测虽然也是在每一个时钟上升沿去检测判断sig1的情况，但是检查结果仅在“|=>”和“|->”前的表达式为真的情况下才会输出，不会出现前例中的每个采样时钟上升沿都输出信息的现象。在这个示例中，我们注意到在属性property中使用了一些特殊的语法结构，其具体含义如下：
| 示例 | 说明 |
| property sp1; sig1 |=> sig2; endproperty // sp1 property sp2; sig3 |-> sig4; endproperty // sp2 property sp3; sig5 ##n sig6; endproperty // sp3
property pr1; clocking_event sp1 |=> sp2 |-> sp3; endproperty // pr1
assert property(pr1)； | |=>和|->是蕴含操作符，分别表示非交叠蕴含（Non-Overlapped Implication）和交叠蕴含（Overlapped Implication），位于|=>和|->左侧的称为“先行算子（Antecendent）”，右侧的称为“后续算子（Consequent）”，先行算子为约束条件，当先行算子匹配成功时，后续算子才会被计算，如果此时后续算子也匹配成功了，那么该断言“真”成功，如果此时后续算子计算失败，那么该断言失败。这里需要注意的是如果先行算子匹配失败，那么整个属性并不会认为失败，会被认为“成功”，这个成功为“假”成功，叫做空成功（Vacuous Success）。同时需要注意蕴含操作只能使用在property或者assert property中，不能在sequence中使用。 |
| ##n，表示延迟n个采样周期 | |
| 不管是sequence还是property都需要assert property才会被激活进行check，否则他们本身在设计中是不会执行的。 | |
| 这里的sig1、sig2、sig3、sig4等可以为各种复杂的序列表达式，从而可以实现复杂的序列功能。 |
这里需要非常注意的是，“|=>和|->”不能用于sequence中，作为蕴含操作符的|=>和|->语法结构完全一样，都可以用if-else结构替换，但是从示例中可以看到两者的断言成功时间不一样，那么这个差别怎么表现出来呢？请看下例。
【示例】
`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig1,sig2,sig3;
initial begin
clk = 1'b0;
forever #1 clk = ~clk;
end
initial begin
sig1 = 1'b0;sig2 = 1'b0;sig3 = 1'b0;
#2 sig1 = 1'b1;sig2 = 1'b1;
#2 sig1 = 1'b0;sig3 = 1'b1;
#4 $stop;
end
// ｜=>
property pr0;
@(posedge clk) sig1 |=> sig3;
endproperty // pr0
// ｜->
property pr1;
@(posedge clk) sig1 |-> sig2;
endproperty // pr1
// ｜-> ##1
property pr2;
@(posedge clk) sig1 |-> ##1 sig3;
endproperty // pr2
a1 : assert property(pr0) $display("@%0t | p0 : PASSED!",$time);
else $display("@%0t | p0 : FAILED!",$time);
a2 : assert property(pr1) $display("@%0t | p1 : PASSED!",$time);
else $display("@%0t | p1 : FAILED!",$time);
a3 : assert property(pr2) $display("@%0t | p2 : PASSED!",$time);
else $display("@%0t | p2 : FAILED!",$time);
endmodule // top_tb 【仿真结果】 
a1和a3的检查结果一样，这是因为“｜=>”和“｜-> ##1”等效，两者都是在sig1（先行算子）匹配后，在下一个时钟周期sig3（后续算子）匹配，断言成功。a2中，sig1和sig2在同一个时钟周期计算，如果此时sig1和sig2同时满足要求，则断言成功。由a1、a2和a3的仿真结果可以看出，“｜=>”描述的是先行算子比后续算子提前一个时钟周期，“｜->”描述的是先行算子和后续算子在同一个时钟进行计算判断匹配情况。这里有个小建议：在编写断言时尽量使用“｜->”而不是“｜=>”，因为你可以通过“｜->”后增加时钟数实现“｜=>”的功能，但是不能通过“｜=>”实现“｜->”的功能。下面两图示意了“｜=>”和“｜->”的判断机理。
s1 |->s2
s1 |=> s2
