SV assertion for random toggle of output

Hi,

I have a scenario where the IP gives output which has clock type of toggling but the pulse width are not uniform.

How will i verify the toggling using SV assertion? Any idea ?

Regards
Taahir

In reply to syed taahir ahmed:

You need to provide more details. Such as:

  1. Is your clock faster than this output signal?
  2. Since you say “random toggle” - how random is that? Is it possible to specify that in English? Only then it makes sense to attempt to capture that in SVA.

Regards
Srini
www.verifworks.com

In reply to Srini @ CVCblr.com:

In reply to syed taahir ahmed:
You need to provide more details. Such as:

  1. Is your clock faster than this output signal?
  2. Since you say “random toggle” - how random is that? Is it possible to specify that in English? Only then it makes sense to attempt to capture that in SVA.
    Regards
    Srini
    www.verifworks.com

Hello Srini,

To clearly explain the scenario, I’ll put this statement’s.

  1. The IP is configured with values due to there’s output which is similar to clock toggles.
  2. The period of the output is not fixed, it can change but i have to verify it that it’s toggling at any point of time.
  3. there no reference to capture the period, as it varies intermediately.

Regards
Taahir

In reply to syed taahir ahmed:

Based on the limited understanding of your requirement, below is an attempt:



module chk;
  timeunit 1ns;
  timeprecision 1 ns;

  // SVA need a ref clock, so am generating one at 2 ns period
  // Tweak this period as per your design speed
  bit clk;
  always #1 clk = ~clk;
  
  default clocking @(posedge clk);
  endclocking

  // Assuming that within 20 ns after your IP is configured, there will be toggles. 
  // Again tweak the numbers as necessary
  property p_chk_random_toggle;
    after_ip_is_configured |-> ##[1:10] $rose(random_out_sig) ##[1:10] $fell(random_out_sig)
  endproperty : p_chk_random_toggle

Sorry for the vague code - you need to refine it with your spec (as the spec provided above seems incomplete).

Regards
Srini
www.verifworks.com

In reply to Srini @ CVCblr.com:

In reply to syed taahir ahmed:
Based on the limited understanding of your requirement, below is an attempt:


module chk;
timeunit 1ns;
timeprecision 1 ns;
// SVA need a ref clock, so am generating one at 2 ns period
// Tweak this period as per your design speed
bit clk;
always #1 clk = ~clk;
default clocking @(posedge clk);
endclocking
// Assuming that within 20 ns after your IP is configured, there will be toggles. 
// Again tweak the numbers as necessary
property p_chk_random_toggle;
after_ip_is_configured |-> ##[1:10] $rose(random_out_sig) ##[1:10] $fell(random_out_sig)
endproperty : p_chk_random_toggle

Sorry for the vague code - you need to refine it with your spec (as the spec provided above seems incomplete).
Regards
Srini
www.verifworks.com

Thanks Srini, i have got an idea based on your inputs.

I’ll update you soon once I’ll implement on this.

Regards
Taahir

In reply to Srini @ CVCblr.com:

Hi Srini,

I tired to implement the scenario but looks like i am yet to get the understanding.

Following is the code and snap.

property  main_test1_check;
      @(negedge clk_ref)
      disable iff(!check_en[0]) 1 |-> ##1 $rose(  ip_out_main ) ##1 $fell(ip_out_main);
      endproperty
      assert_main_test1_check  :  assert property(main_test1_check) begin
      $dsiplay ("Clock is toggling\n");
      end else begin
      $error ("Asserion failed for clock\n");
      end

Snap:: https://goo.gl/photos/d3kaGttyfGUfsJPZ9

Here the output is in between the ref clock and it has to check that ip_out_main toggling.

Regards
Taahir

In reply to syed taahir ahmed:

The way the code is written I guess you will see many failures

Can you confirm what you would expect in that waveform? Meaning when do you expect a pass and when a fail?

Srini
www.verifworks.com

In reply to Srini @ CVCblr.com:

Yes i am seeing the failures.

The Pass condition is the output signal ip_out_main should be toggling.
Failure should be only it is not toggled and ‘x’.

Regards,
Taahir

In reply to syed taahir ahmed:

Can you point in that waveform sample pass time and fail time stamps?

In reply to Srini @ CVCblr.com:

Srini, it’s failing for every cycle of the ref clock check.

# ** Error: Asserion failed for clock
#    Time: 26638 ns Started: 26637 ns 
# ** Error: Asserion failed for clock
#    Time: 26639 ns Started: 26638 ns 
# ** Error: Asserion failed for clock
#    Time: 26640 ns Started: 26639
# ** Error: Asserion failed for clock
#    Time: 26641 ns Started: 26640 ns 
# ** Error: Asserion failed for clock
#    Time: 26642 ns Started: 26641 ns

Snap:: https://goo.gl/photos/ebEb7FJAq6g5Fgoc8

Regards
Taahir

In reply to syed taahir ahmed:

That’s known from your code, can you “specify” when do you want it to pass and when fail?

I’m yet to understand your requirement

Srini

In reply to Srini @ CVCblr.com:

In reply to syed taahir ahmed:
That’s known from your code, can you “specify” when do you want it to pass and when fail?
I’m yet to understand your requirement
Srini

Pass condition:: The signal should be toggling(Just the toggles happening).
Fail condition:: If the Signal is not toggling at all.

Regards,
Taahir

In reply to Srini @ CVCblr.com:

Srini,

Please let me know what can be implementation?

Regards
Taahir

In reply to syed taahir ahmed:

Try the below:


  property  main_test1_check;
      @(negedge clk_ref)
      $rose(check_en[0])  |-> ##[1:10] $rose(ip_out_main ) ##[1:10] $fell(ip_out_main);
  endproperty
  assert_main_test1_check  :  assert property(main_test1_check) begin
      $dsiplay ("Clock is toggling\n");
  end else begin
      $error ("Asserion failed for clock\n");
  end

I’m using 1:10 range - you will need to tweak it as per your spec. Also is the negedge used for “race avoidance”? If so, don’t worry, use posed and let SVA sampling semantics do the trick for you.

Good Luck
Srini
www.verifworks.com

In reply to Srini @ CVCblr.com:

Sure Srini, i go head with the implementation.

One doubt, since $rose and $fell and since the clk_ref edge’s are not aligned with out signal, will assertions catch the rise and fall of the output toggle?

Regards
Taahir

In reply to syed taahir ahmed:

By definition $rose/$fell will sample with reference clock’s edge. So no issues here.

Regards
Srini
www.verifworks.com

In reply to Srini @ CVCblr.com:

In reply to syed taahir ahmed:
By definition $rose/$fell will sample with reference clock’s edge. So no issues here.
Regards
Srini
www.verifworks.com

Srini,

I have coded in this way and assertions are passing.

sequence hi_to_lo
(ip_out_main === 1'b1) |-> #[1:500] (ip_out_main === 1'b0)
endsequence

sequence lo_to_hi
(ip_out_main === 1'b0) |-> #[1:500] (ip_out_main === 1'b1)
endsequence



property  main_test1_check;
@(posedge clk_ref)
   hi_to_lo or lo_to_hi
endproperty

Regards
Taahir

In reply to Srini @ CVCblr.com:

In reply to syed taahir ahmed:
By definition $rose/$fell will sample with reference clock’s edge. So no issues here.
Regards
Srini
www.verifworks.com

Srini,

I have coded in this way and assertions are passing.

sequence hi_to_lo
(ip_out_main === 1'b1) |-> #[1:500] (ip_out_main === 1'b0)
endsequence

sequence lo_to_hi
(ip_out_main === 1'b0) |-> #[1:500] (ip_out_main === 1'b1)
endsequence



property  main_test1_check;
@(posedge clk_ref)
   hi_to_lo or lo_to_hi
endproperty

Regards
Taahir

In reply to syed taahir ahmed:

Strange as sequences do not allow implication operator as per LRM.

Srini
www.verifworks.com

In reply to Srini @ CVCblr.com:

In reply to syed taahir ahmed:
Strange as sequences do not allow implication operator as per LRM.
Srini
www.verifworks.com

Srini,

You are right, it was typo here.

sequence hi_to_lo
(ip_out_main === 1'b1) #[1:500] (ip_out_main === 1'b0)
endsequence

sequence lo_to_hi
(ip_out_main === 1'b0) #[1:500] (ip_out_main === 1'b1)
endsequence



property  main_test1_check;
@(posedge clk_ref)
   hi_to_lo or lo_to_hi
endproperty

Regards
Taahir