SVA 中的bind为何不起作用？

crystal_duan

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);

bind  xx  xx_asser_chk  chk_u(clk,select,a,b,c,o);


endmodule

module  xx_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;
@(posedge  clk)(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，为什么呀？

crystal_duan

回复 1# crystal_duan

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  xx_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;


@(posedge  clk)((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);

bind  xx  xx_asser_chk  chk_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;


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


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


endmodule

acgoal

回复 2# crystal_duan


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