SVA中的内嵌函数

在SVA中存在着大量的内嵌函数，这些函数在实现对特定状态数据检查非常有用，本文将示例其中几种常用的内嵌函数，这几个内嵌函数为：$onehot\$onehot0\$isunknown\$countones等。

1 $onehot(expression)

该函数主要用于在任意给定的采样事件，表达式最终结果中不管其他位为不定态还是高阻态，只要有一位且仅有一位为高时，该函数即返回真。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0;
logic [7:0] sig1;

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

initial begin
       sig0 = 1'b0;   sig1 = 8'b0000_0000;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_0001;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_0011;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_00x0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_00z0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_10x0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_10z0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_0000;
    #6 $stop;
end

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

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

【仿真结果】

示例中，在第一次检查时，sig1只有一位为高，所以$onehot返回真，属性匹配；第二次检查时sig1中有2位为高，所以$onehot返回假，属性不匹配；第三次检查sig1中sig1[1]为不定态，sig1其他位为低，$onehot返回假，属性不匹配；第四次检查sig1中sig1[1]为高阻态，sig1其他位为低，$onehot返回假，属性不匹配；第五次检查sig1中sig[1]为不定态，sig1[3]为高电平，即sig1中有1位为高电平，所以$onehot返回真，属性匹配；第六次检查sig1中sig1[1]为高阻态，sig1[3]为高电平，即sig1中有1位为高电平，所以$onehot返回真，属性匹配；第七次检查sig1所有位都为低电平，所以$onehot返回假，属性不匹配。

2 $onehot0(expression)

该函数主要用于在任意给定的采样事件，表达式最终结果中不管其他位为不定态还是高阻态，只要有一位为高或者没有任何位为高时，该函数即返回真。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0;
logic [7:0] sig1;

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

initial begin
       sig0 = 1'b0;   sig1 = 8'b0000_0000;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_0001;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_0011;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_00x0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_00z0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_10x0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_10z0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_0000;
    #6 $stop;
end

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

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

【仿真结果】

示例中，在第一次检查时，sig1只有一位为高，所以$onehot0返回真，属性匹配；第二次检查时sig1中有2位为高，所以$onehot0返回假，属性不匹配；第三次检查sig1中sig1[1]为不定态，sig1其他位为低，$onehot0返回真，属性匹配；第四次检查sig1中sig1[1]为高阻态，sig1其他位为低，$onehot0返回真，属性匹配；第五次检查sig1中sig[1]为不定态，sig1[3]为高电平，即sig1中有1位为高电平，所以$onehot0返回真，属性匹配；第六次检查sig1中sig1[1]为高阻态，sig1[3]为高电平，即sig1中有1位为高电平，所以$onehot0返回真，属性匹配；第七次检查sig1所有位都为低电平，所以$onehot0返回真，属性匹配。

3 $isunknown(expression)

该函数用于检验表达式最终结果中的各位中是否有x或者z。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0;
logic [7:0] sig1;

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

initial begin
       sig0 = 1'b0;   sig1 = 8'b0000_0000;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_0001;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_0011;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_00x0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_00z0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_10x0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_10z0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_0000;
    #6 $stop;
end

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

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

【仿真结果】

示例中，当sig1中存在X或者Z时，$isunknown就会返回真，此时属性检查匹配。当sig1中不存在X或者Z时，$isunknown就会返回假，此时属性检查不匹配。

4 $countones(expression)

该函数主要用于获得信号中电平为高的位的个数。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0;
logic [7:0] sig1;

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

initial begin
       sig0 = 1'b0;   sig1 = 8'b0000_0000;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_0001;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_0011;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_00x0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_00z0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_10x0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_10z0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 8'b0000_0000;
    #6 $stop;
end

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

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

【仿真结果】