Reset awareness when using 'sequence.triggered

Question

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".

Let's take a simple example:

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:

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.

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

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;

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");

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

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?

Answer 1

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

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");

Proof of concept: https://www.edaplayground.com/x/6Luf