[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?

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
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!

6

@dave_59 Hi Dave! found one more way to do this using intersect alone,
just wanted to share and make sure I am not making any mistakes here.

b[->1] ##1 !b[->1] to check for one pulse

##0 !b[*1:$] to make sure ‘b’ doesn’t rise again

Naturally after adding this the start and endpoints are aligned properly.

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

7

This sequence will match even if b is asserted continuously for more than 1 clock

As a result this doesn’t check that b was asserted for only clock

bit clk , a , b;  

always #5 clk = !clk;
 
// Property 'p1' :: 
// @(posedge clk) $rose(a) |-> (b[->1] ##1 !b[->1] ##0 !b[*1:$]) intersect (a[*15])
  
  assert property(p1) $display("T:%0t Pass",$time);
                else  $display("T:%0t Fails",$time);
    
  initial begin:B1
    #14 a = 1;    
    // 'b' is sampled high at T: 55 & T: 65 
    #40 b = 1;  // T: 54  
    #20 b = 0;  // T: 74.  
    #80;        // T: 154
    #2 $finish();
  end

Assertion would pass at T: 155 although b was sampled high at T: 55 & T: 65 ( i.e 2 clocks )

One solution that I could think of

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

With B1 we observe assertion failure at T: 65

initial begin:B2
    #14 a = 1;    
    // 'b' is Never sampled high 
    #140 ;        // T: 154
    #2 $finish();
  end

With B2 we observe assertion failure at T: 155 as b was never asserted

initial begin:B3
    #14 a = 1;    
    #40 a = 0;  // 'a' was asserted only for 4 clocks  
    #20 b = 0;    
    #80;        // T: 154
    #2 $finish();
  end

With B3 we observe assertion failure at T: 55 as soon as a was de-asserted