在断言中使用“sequence.triggered”时重置感知

我有一些断言使用triggered序列的性质。这对于检查“当 X 发生时，Y 一定在过去的某个时间发生”形式的属性很有用。

让我们举一个简单的例子：

给定三个信号，a, b and c, c仅允许在以下情况下走高：a3 个周期前为高，并且b2 个周期前为高位。这是满足此属性的迹：

为了能够检查这一点，我们需要一个辅助（时钟）序列，该序列应该在c是合法的：

  sequence two_cycles_after_a_and_b;
    @(posedge clk)
      a ##1 b ##2 1;
  endsequence

然后我们可以在断言中使用这个序列：

  c_two_cycles_after_a_then_b : assert property (
      c |-> two_cycles_after_a_and_b.triggered )
    $info("Passed");

这个断言在大多数情况下工作得很好，但是在处理重置时它会变得混乱。

假设我们还有一个复位信号，该信号恰好在以下时钟周期内变为活动状态：b and c:

在这种情况下，最简单的方法是在断言之外、在default disable iff clause:

  default disable iff !rst_n;

预期是这样，因为重置之前已激活c, the a ##1 b之前发生的事情不算数，并且断言失败。然而，事实并非如此，因为序列的评估与重置无关。

要实现此行为，必须使序列能够重置：

  sequence two_cycles_after_a_and_b__reset_aware;
    @(posedge clk)
      rst_n throughout two_cycles_after_a_and_b;
  endsequence

并且断言需要使用重置感知版本：

  c_two_cycles_after_a_then_b__reset_aware : assert property (
      c |-> two_cycles_after_a_and_b__reset_aware.triggered )
    $info("Passed");

第二个断言确实会失败，因为two_cycles...由于发生重置，序列将不匹配。

这显然是有效的，但它需要更多的努力，并且需要重置才能成为序列/属性的组成部分，而不是在每个范围的基础上进行控制。在这种情况下，有没有其他方法可以实现重置意识，更接近于使用disable iff?

我能想到的最好的解决方案是添加一些辅助代码来示例rst_n并将其保持足够低的时间，以便时钟对其进行采样。

always @(posedge clk, negedge rst_n) begin
  if(!rst_n) smpl_rst_n <= 1'b0;
  else       smpl_rst_n <= 1'b1;
end

然后使用通用序列进行重置感知，使用smpl_rst_n以及对目标序列的引用。

sequence reset_aware(sequence seq);
  @(posedge clk)
  smpl_rst_n throughout seq;
endsequence

最终断言的工作原理如下：

a_two_cycles_after_a_then_b__reset_aware : assert property (
  c |-> reset_aware(two_cycles_after_a_and_b).triggered )
$info("Passed");

概念证明：https://www.edaplayground.com/x/6Luf https://www.edaplayground.com/x/6Luf