SystemVerilog门控时钟场景下$past采样异常致断言失败咨询

测试所用的断言代码如下：

p1: assert property (@(posedge clk) ($past(b, 2, c)) === 0);

VCS仿真过程中，该断言在13s、15s、17s等时刻报失败。核心疑问：11s时刻$past(b, 2, c)返回值为0（对应7s时刻b的采样值），13s时刻门控信号c的值为0，为什么此时$past(b, 2, c)采样到的是9s时刻的b值，导致断言失败？

你对$past()第三个门控参数的语义理解存在偏差，这是断言不符合预期的核心原因：

• 根据SystemVerilog LRM标准，$past(expr, N, gating_en)的执行逻辑是：每到当前时钟采样沿（这里是posedge clk），就向过去的时钟沿回溯，仅统计gating_en采样值为1的时钟沿，数够N个满足gating_en为1的时钟沿后，返回对应位置expr的采样值。

这个回溯计算过程和当前时钟沿的gating_en是0还是1没有任何关系，只要到达posedge clk采样点，断言就会执行完整的回溯计算，不会因为当前c为0就沿用之前的计算结果，也不会跳过本次断言检查。

• 对应13s时刻的场景拆解：13s是posedge clk采样点，断言正常触发执行，开始回溯统计c为1的时钟沿：往回找到的第一个c=1的时钟沿是11s，第二个c=1的时钟沿是9s，因此$past(b,2,c)直接返回9s时刻b的采样值，和你预期的7s时刻值不一致，所以断言失败。
• 15s、17s时刻的失败逻辑完全一致：每个时钟沿都会独立回溯统计历史上c为1的沿，不会受当前c电平影响。

如果你预期的逻辑是「仅当c为高时才采样检查，c为低时不触发断言」，需要把c作为断言的前置条件，而不是$past的门控参数，修改代码如下：

p1: assert property (@(posedge clk) c |-> ($past(b, 2) === 0));

上述代码的逻辑是：仅当当前采样沿c为1时，才检查2个时钟周期前的b值是否为0；c为0时断言不执行检查，不会报错。

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