SVA 中的bind为何不起作用？

module xx(select,a,b,c,o);
input [1:0]select;
input [4:0] a,b,c;
output [4:0]o;
reg [4:0]o;
always@(a or b or c or select)
begin
case(select)
1=a;
2=b;
3=c;
default:o=a;
endcase
end
always_comb
begin
assert_select: assert ((select == 1)&&(o==a));
end
endmodule
module testbench;
reg[1:0]select;
reg [4:0]a,b,c;
wire [4:0] o;
reg clk,rst_n;
integer i;
initial begin
a=4;b=5;c=6;
rst_n = 0;
clk = 0;
#2;
rst_n= 1;
#3;
clk = 1;
for(i=0;i<100;i=i+1)
#5 clk = ~clk;
$stop;
end
always @(posedge clk or negedge rst_n)
begin
if(~rst_n)
select <=0;
else
select <=select+1;
end
xx xx_u(select,a,b,c,o);
bindxxxx_asser_chkchk_u(clk,select,a,b,c,o);

endmodule
modulexx_asser_chk(clk,select,a,b,c,o);
input clk;
input [1:0]select;
input [4:0] a,b,c;
input [4:0]o;

property chk_sel;
@(posedgeclk)(select == ($past(select)+1));
endproperty

assert_sel: assert property (chk_sel);
cover_sel: cover property (chk_sel);
endmodule
在modelsim中运行：
vlog -sv -cover bset +acc=a xx.sv
vsim -assertcover -coverage testbench
run 60ns
运行结果：fail_count、pass_count、active count全部为0，为什么呀?

module xx(select,a,b,c,o);
input [1:0]select;
input [4:0] a,b,c;
output [4:0]o;
reg [4:0]o;
always@(a or b or c or select)
begin
case(select)
1=a;
2=b;
3=c;
default:o=a;
endcase
end
always_comb
begin
assert_select: assert ((select == 1)&&(o==a));
end

endmodule

modulexx_asser_chk(clk,select,a,b,c,o);
input clk;
input [1:0]select;
input [4:0] a,b,c;
input [4:0]o;

property chk_sel;

@(posedgeclk)((select == 1)&&(o==a));// (select == ($past(select)+1));
endproperty

assert_sel: assert property (chk_sel);
cover_sel: cover property (chk_sel);
endmodule
module testbench;
reg[1:0]select;
reg [4:0]a,b,c;
wire [4:0] o;
reg clk,rst_n;
integer i;
initial begin
a=4;b=5;c=6;
rst_n = 0;
clk = 0;
#2;
rst_n= 1;
#3;
clk = 1;
for(i=0;i<100;i=i+1)
#5 clk = ~clk;
$stop;
end
always @(posedge clk or negedge rst_n)
begin
if(~rst_n)
select <=0;
else
select <=select+1;
end
xx xx_u(select,a,b,c,o);
bindxxxx_asser_chkchk_u(clk,select,a,b,c,o);

property sel_seq;
@(posedge clk)(select ==0)|=>(select ==1)|=> (select==2)|=> (select==3)|=> (select==0);
endproperty
assert_seq: assert property (sel_seq);
cover_seq: cover property (sel_seq);

property chk_sel1;

@(posedgeclk) if($past(select)==3)(select == 0)elseif($isunknown($past(select)))(select ==0) else(select == ($past(select)+1));
endproperty

assert_sel1: assert property (chk_sel1);
cover_sel1: cover property (chk_sel1);

endmodule

你确定能bind?你bind的那个模块xx，可是没有clk的呢。端口声明不一样吧，居然没报错?