[SVA Question] Signal 'b' has to toggle only once within 10cycle window of signal 'a' after 'a' is asserted

SystemVerilog
, ,
1

Let me know if question is not clear:

I tried a within construct but as we know it not strict condition for just ONE occurrence if Toggle.

@ (posedge clk) $rose(a) |-> (b[->1] ##[*1:$] !b[*0:$] ) within (a[*10])

So, I tried a intersect construct with first_match to make it more stricter:

@ (posedge clk) $rose(a) |-> first_match(##[0:$] $rose(b) ##[1:$] !b[*1:$]) intersect (a[*10]);

The above is failing at a different point that says offending !b at a point where b is actually 0 in the waves.

One more idea I had was to use ‘count’ but i felt cycle level accurate solution will be universally applicable.

Any ideas? anyone stuck with this for days :frowning:

2

It would be helpful if you could create a small test case that demonstrates the problem.

Also, when you say toggle, do you really mean asserted/rose? And is it a requirement that a must remain asserted for 10 cycles? can there be overlapping windows?

1 Like
3

Hi @dave_59 thanks for replying:

when you say toggle, do you really mean asserted/rose?
Yes we want only a single pulse ( posedege + negedge ) of b within the window.

And is it a requirement that a must remain asserted for 10 cycles? can there be overlapping windows?
Yes a has to be continuously 1 ie, a[*10]

Test Case Summary

Case 1: Single Pulse (Expected Pass)

In this scenario, signal b rises and falls exactly once while a remains asserted for a continuous window.

  • a: 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1
  • b: 0 0 0 0 0 1 1 1 1 1 1 1 0 0 0 0

Case 2: Double Pulse (Expected Fail)

In this scenario, signal b rises and falls twice while a is asserted. This should trigger a failure.

  • a: 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1
  • b: 0 0 0 0 0 1 1 0 0 1 1 1 0 0 0 0

Core Constraint

We should only have 1 pulse of ‘b’ within the window of 10 (or n cycles) of ‘a’ being 1

The within construct is not strict for multiple matches and is passing.
1 pulse → within → passing
2 pulse → within → again passing since within is not strict 1 match but we want ONLY 1 match.
** Also first_match wont work since the 2nd pulse is also identical and it eventually becomes the first_match for the final matching logic.

***Note ***
Refer to the property throughout_ab
Also i made it *15 cycles in the EDA playground to match the 2 pulses of b.

Let me know if its still not clear I can add more info.

4 
sequence cycles(n);
    ##1 1[*n];   // cycle window
endsequence

sequence one_pulse(sig);
    $rose(sig) ##0 $fell(sig)[->1];
endsequence

property within_ab;
  @(posedge clk)
  $rose(a) |-> 
    (
      // a stays high
      a throughout cycles(10)
      and
      // one pulse of b in the window
      one_pulse(b) within cycles(10)
      and
      // prevent another rise of b after the first pulse
      not (one_pulse(b) ##0 b[->1]) within cycles(10)
    );
endproperty
1 Like
5

Thanks @dave_59 - this works!
I was trying to write it in the using this a[*10]

Didn’t realize :

  • a[*10] can we written as a throughout cycles(10)!!!
  • Combination of AND and THROUGHOUT creates a magic like this

that’s great learning for me - thank you so much!