How does ## interact with $past

SystemVerilog
1

Hi All

We are trying to encode a specific behavior in SVA and getting an odd assertion fail that makes me think
we don’t understand the behavior of the ## operator when combined with $past.

Here is the waveform - its a simple case, and the assertion violates at time 440/480

1381×804 43.9 KB

The assertion is simply

@(posedge clk)
( $past(launch) != launch) → ##1 ( $past(capture) == capture )

in some cases, we extend it to two cycles using [*2]. The assertion is expected to say “launch” changes state,
then “capture” should not change state in the next cycle. I don’t know if it’s encoded wrong, this seems to work
in most other cases, but in this case the design does a clock stretch and we don’t understand why the assertion
triggers.

Thanks all

Sam

2

In reply to sama:

@(posedge clk)
( $past(launch) != launch) → ##1 ( $past(capture) == capture )

Your assertion is correct.


// same assertion 
@(posedge clk) $changed(launch) |=> $stable(capture);

Per your waveform, the assertion should PASS because at 440 capture the signal launch changes in the NDA region, but it is sampled in the Preponed region where it is ZERO.
See How does Observed region trigger a loop back to Active region? - SystemVerilog - Verification Academy

in some cases, we extend it to two cycles using [*2]. The assertion is expected to say “launch” changes state, then “capture” should not change state in the next cycle. I don’t know if it’s encoded wrong, this seems to work in most other cases, but in this case the design does a clock stretch and we don’t understand why the assertion

I believe that your issue is how your clk relates to the signal changes. You elongate the clk. The assertion behaves as if the Proponed region of the clk samples the capture after it has changed. In other words, it looks like there is an offset in the clocks such that the NDA (or Active) region of when your capture falls just before the rose of clk when clk is elongated.
Suggestion: Analyze that logic and make sure that the clk is identical to the ones used in the assertion sampling of all the signals.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr