在线咨询
eetop公众号 创芯大讲堂 创芯人才网
切换到宽版

EETOP 创芯网论坛 (原名:电子顶级开发网)

手机号码,快捷登录

手机号码,快捷登录

找回密码

  登录   注册  

快捷导航
搜帖子
查看: 3550|回复: 2

[求助] SVA 中的bind为何不起作用?

[复制链接]
发表于 2015-1-28 07:39:13 | 显示全部楼层 |阅读模式

马上注册,结交更多好友,享用更多功能,让你轻松玩转社区。

您需要 登录 才可以下载或查看,没有账号?注册

x
本帖最后由 crystal_duan 于 2015-1-31 12:07 编辑

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,为什么呀?
 楼主| 发表于 2015-1-28 22:36:33 | 显示全部楼层
本帖最后由 crystal_duan 于 2015-1-31 12:06 编辑

回复 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
发表于 2015-2-27 17:23:49 | 显示全部楼层
回复 2# crystal_duan


   你确定能bind?你bind的那个模块xx,可是没有clk的呢。端口声明不一样吧,居然没报错?
您需要登录后才可以回帖 登录 | 注册

本版积分规则

关闭

站长推荐 上一条 /1 下一条


小黑屋| 手机版| 关于我们| 联系我们| 在线咨询| 隐私声明| EETOP 创芯网
( 京ICP备:10050787号 京公网安备:11010502037710 )

GMT+8, 2024-11-14 14:29 , Processed in 0.016507 second(s), 8 queries , Gzip On, Redis On.

eetop公众号 创芯大讲堂 创芯人才网
快速回复 返回顶部 返回列表