含if...else的SystemVerilog断言出现空匹配问题求助

首先明确：SystemVerilog断言完全支持if-else结构，你的问题并非源于使用if-else，而是else分支的序列逻辑或采样细节导致的空匹配触发。

问题分析 #

你的断言逻辑是：当APB写命令命中指定地址时，根据pwdata_dm[17]的值，要么在0-1个周期内检测abs_stat_busy的上升沿，要么连续3个周期检测abs_stat_busy保持稳定。

你提到的空匹配（vacuous match）通常发生在先行算子（|->左侧条件）为假时，断言直接判定为成功；但你描述的场景是先行算子为真（已进入else分支）仍触发空匹配，大概率是以下原因：

• $stable(abs_stat_busy)[*3]的采样异常：$stable依赖当前采样值与上一周期采样值的比较，若复位后首次触发断言，上一周期的abs_stat_busy状态不确定，可能导致序列不满足，进而触发空匹配。
• 断言执行期间复位信号rst_a生效：disable iff(rst_a)会终止断言执行，这种终止可能被误判为空匹配。

解决方案 #

改用显式的数值比较替代$stable，通过局部变量捕捉先行时刻的abs_stat_busy值，后续周期直接对比该值，避免$stable的采样不确定性：

property wr_cmd_will_set_busy ;
    logic [abs_stat_busy.width-1:0] busy_snapshot; // 自动匹配信号位宽
    @(negedge pclkdbg) disable iff(rst_a)
    // 先行算子触发时，捕捉当前abs_stat_busy的值
    ( apb_new_trans && (paddr_dm == ADDR_ABS_COMM) && (pwrite_dm), busy_snapshot = abs_stat_busy ) |-> 
    if(pwdata_dm[17])
        ##[0:1] $rose(abs_stat_busy)
    else
        (abs_stat_busy == busy_snapshot)[*3] ; // 连续3周期保持捕捉到的初始值
endproperty

额外验证点 #

• 检查波形中先行算子触发时刻的abs_stat_busy状态，以及后续3个pclkdbg下降沿的该信号值，确认是否真的稳定。
• 确认断言执行期间rst_a未生效，避免disable iff终止断言导致的异常判定。

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