SVA中的与或非（and_or_not）
面对复杂的时序关系，往往一个sequence已经不能完全实现一个复杂功能的检查。为此，在SVA中引入了逻辑操作的概念，与其他语句结构的逻辑操作符不同的是，断言中进行逻辑操作的是序列而不是表达式。在SVA中常用的逻辑操作有三种：and，or，not等。
1 and
“and”可以按照逻辑与的方式组合两个序列，当两个序列都匹配时，整个属性成功。使用方式如下：
property p; sequence_1 and sequence_2; endproperty //p但是在具体使用时需要注意，sequence_1和sequence_2的检查起始点必须一样，但是两者结束的结束点可以不一样，整个属性的成功点以两个sequence中最后一个成功的sequence的匹配点为属性的成功点。
【示例】
`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;sig1 = 1'b1;
#4 sig1 = 1'b0;$stop;
end
// sequence s0
sequence s0;
@(posedge clk) $rose(sig0) ##1 sig1;
endsequence // s0
// sequence s1
sequence s1;
@(posedge clk) $rose(sig0) ##2 sig1;
endsequence // s1
// property
property p;
s0 and s1;
endproperty // p
as0 : assert property(s0) $display("@%0t | s0 : PASSED!",$time);
else $display("@%0t | s0 : FAILED!",$time);
as1 : assert property(s1) $display("@%0t | s1 : PASSED!",$time);
else $display("@%0t | s1 : FAILED!",$time);
ap : assert property(p) $display("@%0t | p : PASSED!",$time);
else $display("@%0t | p : FAILED!",$time);
endmodule 【仿真结果】 
示例中，s0和s1监测的起始点都是在3ns，s0在5ns时断言匹配，但是s1在7ns时才断言匹配，此时“s0 and s1”成功，可见两个序列and时，两个序列的起始点必须一样，但是结束点可以不一样，结束点取决于最后一个匹配的序列。
为了确保设计中的某些同时发生的并行操作能够正确执行，可以使用and操作符实现对这种场景的检查。
2 or
“or”可以按照逻辑或的方式组合两个序列，当两个序列有一个匹配时，整个属性成功。使用方式如下：
property p; sequence_1&nbs***bsp;sequence_2; endproperty //p但是在具体使用时需要注意，sequence_1和sequence_2的检查起始点必须一样，但是两者结束的结束点可以不一样，整个属性的成功点取决于最早匹配成功的sequence，只要两个序列有一个匹配成功，整个属性就认为匹配。
【示例】
`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; sig1 = 1'b1;
#4 sig1 = 1'b0;#2 sig0 = 1'b1;#2 sig0 = 1'b0;
#2 sig1 = 1'b1;#3 sig1 = 1'b0;#4 $stop;
end
//sequece s0
sequence s0;
@(posedge clk) $rose(sig0) ##1 sig1;
endsequence // s0
// sequence s1
sequence s1;
@(posedge clk) $rose(sig0) ##2 sig1;
endsequence // s1
// property p
property p;
s0&nbs***bsp;s1;
endproperty // p
// assertion
as0 : assert property(s0) $display("@%0t | s0 : PASSED!",$time);
else $display("@%0t | s0 : FAILED!",$time);
as1 : assert property(s1) $display("@%0t | s1 : PASSED!",$time);
else $display("@%0t | s1 : FAILED!",$time);
ap : assert property(p) $display("@%0t | p : PASSED!",$time);
else $display("@%0t | p : FAILED!",$time);
endmodule 【仿真结果】 
示例中，在5ns开始s0首先匹配成功，则此时“s0 or s1”匹配成功，此时s1尚未匹配，匹配结束点与s0一样；在13ns处s0没有匹配成功，但是s1在15ns匹配成功，则此时“s0 or s1”匹配成功，且结束点与s1匹配的结束点一样。可见or操作的结束匹配位置为第一个匹配序列的结束点。
3 not
“not”虽然只是对序列结果取反，但是在SVA中，理解not时必须注意反向思维，否则可能混乱。因为not操作的对象为一个序列，所以not操作的起始和结束点与其操作的对象一致。使用方式如下：
property p; not (sequence); endproperty //p括号中为删除内容(但是在具体使用时需要注意，sequence_1和sequence_2的检查起始点必须一样，但是两者结束的结束点可以不一样，整个属性的成功点取决于最早匹配成功的sequence，只要两个序列有一个匹配成功，整个属性就认为匹配。)
【示例】
`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; sig1 = 1'b1;
#4 sig1 = 1'b0;#2 sig0 = 1'b1;#2 sig0 = 1'b0;
#2 sig1 = 1'b1;#3 sig1 = 1'b0;#4 $stop;
end
//sequece s
sequence s;
$fell(sig0) ##1 sig1;
endsequence // s
// property p
property p;
@(posedge clk) not s;
endproperty // p
// assertion
as : assert property(@(posedge clk) s) $display("@%0t | s : PASSED!",$time);
else $display("@%0t | s : FAILED!",$time);
ap : assert property(p) $display("@%0t | p : PASSED!",$time);
else $display("@%0t | p : FAILED!",$time);
endmodule 【仿真结果】 
示例中，在3ns时序列s失败，但是“not s”匹配成功，但是在7ns时，s匹配成功，但是“not s”不匹配，注意这次匹配的起始点在5ns处。可见not是对序列的反向匹配。之所以看到图中“not s”在7ns时存在一个匹配的表示，那是因为s在此刻（7ns）被采样为假。
【示例】
`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2;
initial begin
clk = 1'b0;
forever #1 clk = ~clk;
end
initial begin
sig0 = 1'b0; sig1 = 1'b0; sig2 = 1'b0;
#2 sig0 = 1'b1;#2 sig1 = 1'b1; sig0 = 1'b0;
#2 sig2 = 1'b1; sig1 = 1'b0;#2 sig2 = 1'b0;
#2 sig0 = 1'b1;#2 sig0 = 1'b0;#2 sig1 = 1'b1;
#2 sig1 = 1'b0; sig2 = 1'b1;#4 sig2 = 1'b0;
$stop;
end
// property
property p;
@(posedge clk) not(sig0 ##2 sig1 |-> ##1 sig2);
endproperty // p
// assertion
ap : assert property(p) $display("@%0t | p : PASSED!",$time);
else $display("@%0t | p : FAILED!",$time);
endmodule // top_tb 【仿真结果】 
示例中，在3ns时作为|->的先行算子“sig0 ##2 sig1”为假，此时按照之前定义的蕴含操作的说明，当先行算子为假时，此时的蕴含操作将会为空成功。而在实际的应用中，对空成功的not操作将会表现为一次断言匹配失败，即空成功被not操作认为是一次“真成功”，这样的基于空成功的not操作得到的结果可能不是期望的。在具有蕴含操作断言中使用not操作一定要注意起作用的表达式的组成，否则结果不堪设想。
查看12道真题和解析