在断言中使用“sequence.triggered"时重置意识 [英] Reset awareness when using 'sequence.triggered' in assertion

问题描述

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

I have a few assertions that use the triggered property of sequences. This is useful for checking properties of the form "when X happens, Y must have happened sometime in the past".

举个简单的例子:

给定三个信号，a、b 和 c，c 只允许在 a 在 3 个周期前为高电平，b 在 2 个周期前为高电平.这是满足此属性的跟踪:

Given three signals, a, b and c, c is only allowed to go high if a was high 3 cycles ago and b was high 2 cycles ago. This is a trace that satisfies this property:

为了能够检查这一点，我们需要一个辅助(时钟)序列，它应该在 c 合法的地方匹配:

To be able to check this, we'd need a helper (clocked) sequence that should match at the point where a c is legal:

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

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

We could then use this sequence in an assertion:

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

这个断言在大多数情况下都可以正常工作，但在处理重置时会出问题.

This assertion works fine in most cases, but it's going to go haywire when dealing with resets.

假设我们还有一个复位信号，它恰好在 b 和 c 之间的时钟周期内激活:

Let's say that we also have a reset signal that becomes active exactly in the clock cycle between b and c:

在这种情况下，最简单的方法是在断言之外，在 default disable iff 子句中实现重置感知:

The naive approach in this case would be to implement reset awareness outside of the assertion, inside a default disable iff clause:

  default disable iff !rst_n;

期望是，因为 reset 在 c 之前是活动的，之前发生的 a ##1 b 不计算在内并且断言失败.然而，这不是会发生的事情，因为序列的评估与重置无关.

The expectation would be that, since reset was active before c, the a ##1 b that happened before doesn't count and that the assertion fails. This isn't what happens, though, as the evaluation of the sequence is independent of reset.

要实现此行为，必须使序列具有重置意识:

To achieve this behavior, the sequence must be made reset aware:

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

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

and the assertion needs to use the reset aware version:

  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... 序列将不匹配，因为发生了重置.

The second assertion will indeed fail, because the two_cycles... sequence won't match due to the occurrence of reset.

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

This obviously works, but it requires a lot more effort and it requires reset to become an integral part of the sequences/properties instead of being controlled on a per-scope basis. Is there any other way to achieve reset awareness in this case that is closer to using a disable iff?

推荐答案

我能想到的最佳解决方案是添加一些辅助代码来示例 rst_n 并保持足够低的时间以便它由时钟采样.

Best solution I can come up with is to add a little auxiliary code to sample rst_n and keep it low long enough for it to be sampled by the clock.

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 和对目标序列的引用的重置感知的通用序列.

Then use a generic sequence for the reset aware that uses smpl_rst_n and a a reference to a target sequence.

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

最终断言的工作方式如下:

Final assertion would work as follows:

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

这篇关于在断言中使用“sequence.triggered"时重置意识的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！