SystemVerilog断言错误排查：A保持至B撤销后释放的断言失败

首先，咱们直接说问题核心：你用A throughout !B [->1]的组合，强制要求了B被撤销的那个时钟沿A必须保持高电平，但你的实际需求允许B撤销时A同时变低，这就是A被撤销时断言失败的原因。

咱们拆解一下你的断言逻辑：

1. $rose(A) |->：当A被置位的时钟沿触发断言。
2. A throughout !B [->1]：这里的!B [->1]是指“从触发后开始，第一个出现!B为真的时钟沿”（也就是B被撤销的那个时刻）。而throughout关键字要求A在这个序列的每一个时钟沿（包括序列结束的那个时刻）都必须为高。
3. ##[0:$] !A：要求B被撤销后，0到任意个周期内A最终被撤销。

问题就出在第二步：如果在B被撤销的同一个时钟沿你就把A撤销了，此时!B为真，但A已经是低电平，违反了throughout的要求，断言直接失败，根本轮不到后面的##[0:$] !A生效。而你的需求是“A保持高直到B被撤销”——意思是B撤销之前A必须保持高，B撤销的时刻A可以立刻变低，这和throughout的强制要求冲突了。

修正方案 #

根据你的需求，我们需要调整前半段的约束，让A只需要在B未撤销时保持高，B撤销时允许A变低。有两种常见的写法：

方案1：使用until关键字 #

until的语义正好匹配你的需求：A保持高电平，直到!B为真的时刻，且!B为真时A可以为高或低：

my_assertion : assert property( @(posedge clk) disable iff(reset) 
    $rose(A) |-> (A until !B) ##[0:$] !A ) 
else $display("Assertion failed");

方案2：调整throughout的序列 #

如果更喜欢用throughout，可以把序列改成B[*1:$]，表示B持续为高的所有周期（直到B变低的前一个周期），这样throughout只约束到B撤销前的最后一个周期，B撤销时A就可以自由变低了：

my_assertion : assert property( @(posedge clk) disable iff(reset) 
    $rose(A) |-> (A throughout B[*1:$]) ##[0:$] !A ) 
else $display("Assertion failed");

至于你问的##[0:$]，它的用法是没问题的——它表示在前面的序列完成后，0到任意个周期内!A必须成立，完美符合“A最终需被撤销”的要求。

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