SVA中的条件选择
在SVA中除了可以按照时序特点编写特定的序列和属性外，还可以使用SystemVerilog中一些特定的语法结构实现功能更加复杂的时序，例如条件选择运算符等，本文将以具体的条件选择运算符示例进行说明。
1 条件运算符
SVA中可以在序列和属性的描述中使用条件运算符，从而可以根据不同信号的逻辑选择不同的表达式子进行检查。但是需要注意基于采样事件具有时序控制的表达式不能作为条件运算符的操作数（例如：##n expr），但SVA内建的一些函数可以在条件运算符的表达式中使用。条件运算符在SVA中使用的格式如下：
sequence/property s/p; clocking_event expr_0 ? expr_1 : expr_2; endsequence/endproperty【示例】
`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;sig1 = 1'b0;
#2 sig0 = 1'b0;sig2 = 1'b1;
#4 $stop;
end
// property
property p;
@(posedge clk) $rose(sig0) ? $fell(sig1) : $rose(sig2);
endproperty // p
// assertion
a : assert property(p) $display("@%0t | p : PASSED!",$time);
else $display("@%0t | p : FAILED!",$time);
endmodule // top_tb 【仿真结果】 sig0在1ns时被采样到fell，条件表达式选择$rose(sig2)进行判断，而此时sig2并没有rose，所以此刻断言失败。3ns时，sig0被采样到高电平，$rose(sig0)被判定为真，条件表达式选择$fell(sig1)进行判断，$fell(sig1)被判定为真，此时断言成功。5ns时sig0被采样到低电平，$rose(sig0)被判定为假，条件表达式选择$rose(sig2)进行判断，而此时$rose(sig2)为真，所以此刻断言成功。
【示例】
2 if/else
SVA中允许在使用蕴含操作的属性中使用if/else语句结构，但是其只能出现在蕴含操作的后续算子中，if/else属于一种属性运算符，不能用于sequence表达式中。【示例】
`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;
#2 sig0 = 1'b1;sig1 = 1'b1;#2 sig2 = 1'b1; sig0 = 1'b0; sig1 = 1'b0;
#2 sig3 = 1'b1;sig2 = 1'b0;#2 sig3 = 1'b0;#2 sig0 = 1'b1; sig1 = 1'b0;
#2 sig2 = 1'b1;sig0 = 1'b0; sig1 = 1'b0;#2 sig2 = 1'b0;#2 sig3 = 1'b1;
#2 sig4 = 1'b1;sig3 = 1'b0;#2 sig4 = 1'b0;#2 $stop;
#4 $stop;
end
// property
property p;
@(posedge clk) $rose(sig0) |->
if(sig1)
##1 sig2 ##1 sig3
else
##1 sig2 ##2 sig3
##1 sig4;
endproperty // p
// assertion
a : assert property(p) $display("@%0t | p : PASSED!",$time);
else $display("@%0t | p : FAILED!",$time);
endmodule // top_tb 【仿真结果】 示例中，$rose(sig0)在3ns处被判定为真，此时if中的sig1为高，那么将选择“##1 sig2 ##1 sig3”，整个属性此时相当于是对“$rose(sig0) |-> ##1 sig2 ##1 sig3”进行判断，后续算子匹配，断言成功。$rose(sig0)在11ns处被判定为真，此时if中的sig1为低，那么将选择“##1sig2 ##2 sig3 ##1 sig4”，整个属性此时相当于是对“$rose(sig0) |-> ##1 sig2 ##2 sig3 ##1 sig4”进行判断，后续算子匹配，断言成功。
if/else结构只能作为后续算子出现，在if前不能出现类似“##1”等时序表征的语句使其成为子序列的语句的一部分，但是可以再if/else结构中使用各种序列表达式。同时需要注意，属性中的表达式最后要以“:”结束，所以作为属性中表达式一部分的if/else结构中的任何分支的描述结束时不能使用“:”，示例中25行实际上可以合并到24行从而形成一个子序列，即if/else中的else分支，其中的“:”不属于分支，而是属于整个属性描述结束的标志。
通过上述示例，条件运算符可以在序列和属性的描述中使用，其中可以使用各种布尔表达式包括SVA中的一些内嵌函数，但是其中不能使用具有时序表征的表达式。If/else结构作为一种property中可以使用的结构，其不能成为属性中子序列或者序列的一部分，但是子序列或者序列可以出现在if/else结构中。关于条件运算符和if/else结构的使用要根据具体实际情况合理使用。
if/else结构只能作为后续算子出现，在if前不能出现类似“##1”等时序表征的语句使其成为子序列的语句的一部分，但是可以再if/else结构中使用各种序列表达式。同时需要注意，属性中的表达式最后要以“:”结束，所以作为属性中表达式一部分的if/else结构中的任何分支的描述结束时不能使用“:”，示例中25行实际上可以合并到24行从而形成一个子序列，即if/else中的else分支，其中的“:”不属于分支，而是属于整个属性描述结束的标志。
通过上述示例，条件运算符可以在序列和属性的描述中使用，其中可以使用各种布尔表达式包括SVA中的一些内嵌函数，但是其中不能使用具有时序表征的表达式。If/else结构作为一种property中可以使用的结构，其不能成为属性中子序列或者序列的一部分，但是子序列或者序列可以出现在if/else结构中。关于条件运算符和if/else结构的使用要根据具体实际情况合理使用。
