system-verilog - 在断言中使用“sequence.triggered”时重置意识

Question

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

我们举一个简单的例子：

给定三个信号，a和b，c只有在 3 个周期前为高且2 个周期前为高c时才允许变高。这是满足此属性的跟踪：ab

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

  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和之间的时钟周期内变为活动状态c：

在这种情况下，天真的方法是在断言之外的default disable iff子句内实现重置意识：

  default disable iff !rst_n;

期望是，由于 reset 之前是活动c的，因此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？

score 0 · Accepted Answer

我能想出的最佳解决方案是添加一些辅助代码进行采样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");

1 回答 1