SV断言求助
property dat_clk1_prop;
@(posedge clk1)
$rose(en_1) |=> $stable(dat_clk1) throughout en_1;
endproperty
但是这么写还不是不行，$stable还是只判断一个周期，并不会en_1为高电平的时候都进行判断，请大神帮忙一下，怎么编写。谢谢！
用最容易的方法:
always @(posedge clk1) begin
if (~en_1)
latch_data <= dat_clk1;
else
assert (dat_clk1==latch_data);
end
property p1;@(posedge clk) $rose(en_1) |-> $stable(data);
endproperty: p1
为啥不行?
我这样写了，跑仿真的时候，如果数据和使能同时变化，就是在使能信号的上升沿同时变化，$stable是判别错的
刚才忘记说了，这种写法仅仅在上升沿的时候判断一次，如果en_1很长，data在后面的周期变化，是判断不出来的
我的理解：一般第一个有效的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 前后写反了? 我暂时无法验证。你可以试试看
(en_1 ##1 en_1)|-> $stable(data);
谢谢，我知道这种也行，不知道有没有一种方法，只判断一次的。像你这种情况如果是能信号多周期，数据在使能高电平中间跳变一次，又继续保持稳定，会不断地进行断言，在错误之后的下个时钟周期会判别正确。
“数据在使能高电平中间跳变一次，又继续保持稳定”
这种情况下也能查出来啊，不信你自己试试。
除非你指的是这个跳变小于一个clock tick，那这样的话任何的assertion都查不出来，因为concurrent assertion是基于clock tick的，小于一个tick以内的变化，concurrent assertion没法检查。
是可以查出来，但是如果变回去保持稳定的情况，断言会持续报对。这里的数据变化也是同步的。这次变化断言会判错。但是不是在报错的情况下终止这次判断。如果使能信号很长，数据变化后保持不变，会持续的启动断言。可能你没理解我的意思。
的确没理解你的意思。
就这么说吧：你觉得这个断言哪个地方不满足你的要求了?是有什么情况下无法查出错误来吗?反正我觉得它实现了你要的功能，即：“当en_1为高时，data保持不变。”
如图，图示所示的在使能信号高点平时，进行了错误判断，但是随后的时钟周期就会判断正确。而我想做到在高电平期间只判断一次，或者是在使能信号高电平期间一次判断错误后就不在进行判断。
你是觉得这样影响仿真性能还是怎么的?我倒是想到一个笨办法满足你的要求：
在每个en_1的上升沿的时候$asserton；在每次assertion failed的时候$assertkill。
2楼正解