SVA断言在verif_sig_Stable上升沿时误判问题求助

问题描述 #

需求是当verif_sig_Stable为高电平时，Ready_sig保持稳定。编写的RTL逻辑与断言代码如下：

//Generate signal high during time where signals shouldn't change
always @(posedge FCLK) begin
if(cmd_typeA) begin
    verif_sig_Stable <= 1;
end
else if(cmd_typeB) begin
    verif_sig_Stable <= 0;
end
//else save the status
end

//Assertion
Test_stability : assert property (
 @(verif_sig_Stable )
 verif_sig_Stable |-> $stable(Ready_sig)
 );

实际运行中，当verif_sig_Stable上升沿与Ready_sig同时变化时，断言会误判失败，但RTL的实际行为符合设计要求。

问题分析 #

断言以verif_sig_Stable的跳变沿作为评估触发事件，存在以下逻辑冲突：

• 上升沿触发时，采样的是跳变前的verif_sig_Stable值（0），断言左侧条件不成立，不会检查Ready_sig；
• 下降沿触发时，采样的是跳变前的verif_sig_Stable值（1），左侧条件成立，此时要求Ready_sig与上一次评估周期的值一致，但Ready_sig已在同一delta周期内完成变化，导致断言误判失败。

本质原因是SVA采样机制使用时间步开始时的信号值，而RTL通过组合路径在同一时间步内更新信号，导致评估逻辑与实际行为不匹配。

解决方案 #

方法1：改用时钟触发断言，结合电平条件检查 #

将断言的触发事件改为时钟FCLK，在每个时钟沿检查verif_sig_Stable为高时Ready_sig的稳定性，规避跳变沿采样的问题：

Test_stability : assert property (
 @(posedge FCLK)
 verif_sig_Stable |-> $stable(Ready_sig)
 );

这种方式下，每次时钟沿采样当前的verif_sig_Stable值，若为高则检查Ready_sig相对于上一个时钟沿是否稳定。即使verif_sig_Stable和Ready_sig在同一时钟沿同步变化，也会被正确识别为合法情况——因为稳定期从该时钟沿之后开始，无需检查当前沿的变化。

方法2：用$rose限定触发条件，延迟检查时机 #

如果必须以verif_sig_Stable的跳变作为触发，可通过$rose捕捉上升沿，延迟一个周期后开始检查，并确保稳定期全程满足要求：

Test_stability : assert property (
 @(posedge verif_sig_Stable)
 $rose(verif_sig_Stable) |=> $stable(Ready_sig) throughout (verif_sig_Stable[*1:$])
 );

这里用|=>延迟一个评估周期开始检查，再通过throughout确保verif_sig_Stable保持高的整个期间，Ready_sig都处于稳定状态，规避了上升沿同步变化的误判。

方法3：使用$past明确参考采样值 #

通过$past的第三个参数指定参考事件为verif_sig_Stable的跳变，确保参考的是上一次跳变时的Ready_sig值，而非同一delta周期内的变化后值：

Test_stability : assert property (
 @(verif_sig_Stable)
 verif_sig_Stable |-> Ready_sig == $past(Ready_sig, 1, verif_sig_Stable)
 );

内容的提问来源于stack exchange，提问作者Julien6405