SV断言求助

sofan

要求信号en_1为高电平的时候，数据都保持不变。但是我用$stable只能判断上一个时钟周期的信号和当前时钟周期的信号是否一致。
property dat_clk1_prop;
  @(posedge clk1)
  $rose(en_1) |=> $stable(dat_clk1) throughout en_1;
  endproperty
但是这么写还不是不行，$stable还是只判断一个周期，并不会en_1为高电平的时候都进行判断，请大神帮忙一下，怎么编写。谢谢！

kuolifeng

用最容易的方法:
always @(posedge clk1) begin
    if (~en_1)
        latch_data <= dat_clk1;
    else
        assert (dat_clk1==latch_data);
end

tbb2009

要求信号en_1为高电平的时候，数据都保持不变。但是我用$stable只能判断上一个时钟周期的信号和当前时钟周期 ...
sofan 发表于 2014-1-13 11:06

                               
登录/注册后可看大图

property p1;         @(posedge clk) $rose(en_1) |-> $stable(data);
endproperty: p1

为啥不行？

sofan

回复 3# tbb2009


    我这样写了，跑仿真的时候，如果数据和使能同时变化，就是在使能信号的上升沿同时变化，$stable是判别错的

sofan

property p1;         @(posedge clk) $rose(en_1) |-> $stable(data);
endproperty: p1

为啥 ...
tbb2009 发表于 2014-1-14 00:08

                               
登录/注册后可看大图

刚才忘记说了，这种写法仅仅在上升沿的时候判断一次，如果en_1很长，data在后面的周期变化，是判断不出来的

tbb2009

刚才忘记说了，这种写法仅仅在上升沿的时候判断一次，如果en_1很长，data在后面的周期变化，是判断不出 ...
sofan 发表于 2014-1-14 08:51

                               
登录/注册后可看大图

我的理解：一般第一个有效的en_1下面qualify的data会发生变化，而如果你要check的是后面有效的en_1下面的data的稳定性：

@(posedge clk)  disable iff(reset)  en_1 && $stable(en_1) |-> $stable(data);


如果你要检查所有有效en_1的qualify的data的稳定性：

@(posedge clk) en_1 |-> $stable(data);

或者

@(posedge clk) $rose(en_1) |-> en_1 throughout $stable(data);
这里你说$stable只作用一次，是不是你把 throughout 前后写反了？ 我暂时无法验证。你可以试试看

xiaojigao

(en_1 ##1 en_1)|-> $stable(data);

sofan

(en_1 ##1 en_1)|-> $stable(data);
xiaojigao 发表于 2014-1-15 10:26

                               
登录/注册后可看大图

    谢谢，我知道这种也行，不知道有没有一种方法，只判断一次的。像你这种情况如果是能信号多周期，数据在使能高电平中间跳变一次，又继续保持稳定，会不断地进行断言，在错误之后的下个时钟周期会判别正确。

xiaojigao

回复 8# sofan

“数据在使能高电平中间跳变一次，又继续保持稳定”
这种情况下也能查出来啊，不信你自己试试。

除非你指的是这个跳变小于一个clock tick，那这样的话任何的assertion都查不出来，因为concurrent assertion是基于clock tick的，小于一个tick以内的变化，concurrent assertion没法检查。

sofan

回复 9# xiaojigao


    是可以查出来，但是如果变回去保持稳定的情况，断言会持续报对。这里的数据变化也是同步的。这次变化断言会判错。但是不是在报错的情况下终止这次判断。如果使能信号很长，数据变化后保持不变，会持续的启动断言。可能你没理解我的意思。