Checker for phase of clocks using property

[yoshiko]

I am trying to implement a checker using assertion to check all th clocks of clock divider must be phase alligned w.r.to a strobe signal.
I wrote assertion following way -

// property capable of checking all clocks are phase alligned .
  property clk_phase_pp(logic disab, logic enable, logic do_check, logic div1clk, logic div2clk, logic div4clk, logic strb );
    @(clk) disable iff (disab)
    
      
    (strb)
    |->
    $rose(div1clk)
    |->
    $rose(div2clk)
    |->
    $rose(div4clk)
    
   )
    ;
  endproperty

But this is not working. Please suggest how to check posedge of all the clocks w.r.to strb signal.strb signal is also a pulse equal to div4clk.

[user49]

In reply to yoshiko:

There are many issues with your assertions because of the clocking and sampling in SVA.
I suggest creating 2 stobe signals, one before and and one after the edge you are verifying, and checking th values of the signals of interest, I. E., 0 before, 1 after.
Thus, in an assertion, that would be a 2 clock ckeck of the values of the signals, no rose.

Also see my papers on assertions (below)

SolvingComplexUsersAssertions.pdf

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

See Paper: 1) VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
2) http://systemverilog.us/vf/SolvingComplexUsersAssertions.

[user49]

In reply to ben@SystemVerilog.us:

The waveforms clarified the requirements. You can use multiclocking in the assertion. Thus,

ap_aligned: assert property(
  @(posedge div_clk_strb) 1'b1 ##0 
  @(posedge dfe_clk_src) !clk_div1 && !clk_div2 && !clk_div4 ##0 
  @(negedge dfe_clk_src) clk_div1 && clk_div2 && clk_div4 );   
 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
3. “Using SVA for scoreboarding and TB designs”
   http://systemverilog.us/papers/sva4scoreboarding.pdf
4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
   October 2013 | Volume 9, Issue 3 | Verification Academy
5. SVA in a UVM Class-based Environment
   SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

[yoshiko]

In reply to ben@SystemVerilog.us:

Thank you Ben.
I tried to run the assertion as you mentioned but it is not working . I only want to check posedge of clock.

[user49]

In reply to yoshiko:
From your timing digram

Following @(posedge div_clk_strb)you want to check that that clk_div1, clk_div2 and clk_div4 signals rose after being clocked by dfe_clk_src. This is how I read you timing diagram.
My assertion states that

1. Following @(posedge div_clk_strb)
2. at the next @(posedge dfe_clk_src), the sampling values of lk_div1, clk_div2 and clk_div4 are all zeros
3. This is then followed that at the next @(negedge dfe_clk_src) the sampling values of lk_div1, clk_div2 and clk_div4 are all ONES
   THUS ESSENTIALLY TESTING FOR A ROSE OF THESE 3 SIGNALS.

ap_aligned: assert property(
  @(posedge div_clk_strb) 1'b1 ##0 
  @(posedge dfe_clk_src) !clk_div1 && !clk_div2 && !clk_div4 ##0 
  @(negedge dfe_clk_src) clk_div1 && clk_div2 && clk_div4 );   

You can always create the sampling of these signals using SystemVerilog with the #n delays and test for when they should be all 0’s and all 1’s.
Did I miss something here?
My paper (below) expresses the use of SystemVerilog with tasks to verify complex assertions. Perhaps that paper may give ideas on a different approach.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

1. VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
3. “Using SVA for scoreboarding and TB designs”
   http://systemverilog.us/papers/sva4scoreboarding.pdf
4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
   https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
5. SVA in a UVM Class-based Environment
   https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment

[nimitz_class]

In reply to ben@SystemVerilog.us:

How can this be implemented for two clocks with same frequency but phase shifted by 90 degrees?

[user49]

In reply to nimitz_class:
You can write the assertions one you draw a timing diagram.
Do that first.

[nimitz_class]

realtime t1, t2, half_time_period;

always @(posedge clk1) begin
        t1 = $realtime;
        @(negedge clk1)
        t2 = $realtime - t1;
        half_time_period = t2/2; // half time period of clock 1 divided by 2 to get 90 degree phase shifted time period
end 

property phase_aligned_90_degrees_chk(clk1, clk2, state, realtime half_time_period);
        realtime t1, t2;
        @(posedge clk1) (1, t1=$realtime) ##0 state == 4'h2 |-> @(posedge clk2) (1, t2=$realtime) ##0 ((t2-t1) == half_time_period);
endproperty

I implemented it this way and see a mix of failures and success in the waveform. It’s very confusing, kindly help.

[user49]

In reply to nimitz_class:
Given tht you did not provide a full model, I had to read between the line.
This is a model I created, and it works OK

module m;
  realtime t1, t2, half_time_period;
  bit clk1, clk2;
  initial forever #10 clk1 = !clk1;
  bit[3:0] state=4'b0010; 

  always @(posedge clk1) begin
    t1 = $realtime;
    @(negedge clk1)
     t2 = $realtime - t1;
    half_time_period = t2/2; // half time period of clock 1 divided by 2 to get 90 degree phase shifted time period
  end

  always @(posedge clk1) begin
      realtime full; 
      full=2*half_time_period;
    #half_time_period;
    clk2 <= 1'b1;
    #full;
    clk2 <= 1'b0;
  end

  property phase_aligned_90_degrees_chk(clk1, clk2, state, realtime half_time_period);
    realtime t1, t2;
    @(posedge clk1) (1, t1=$realtime) ##0 state == 4'h2 |-> @(posedge clk2) (1, t2=$realtime) ##0 ((t2-t1) == half_time_period);
  endproperty
  ap_phase_aligned_90_degrees_chk: assert property(phase_aligned_90_degrees_chk(clk1, clk2, state,  half_time_period) );  
    // I implemented it this way and see a mix of failures and success in the waveform. It's very confusing, kindly help.
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
2. Free books: Component Design by Example https://rb.gy/9tcbhl
   Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
3. Papers:

• Understanding the SVA Engine,
  Verification Horizons
• SVA Alternative for Complex Assertions
  https://verificationacademy.com/news/verification-horizons-march-2018-issue
• SVA in a UVM Class-based Environment
  https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

[nimitz_class]

In reply to ben@SystemVerilog.us:

I apologize for not stating my requirements clearly. I just ran your code on EDA playground and got this error:

Compiler version Q-2020.03-SP1-1; Runtime version Q-2020.03-SP1-1; Dec 8 04:32 2021
“testbench.sv”, 28: m.ap_phase_aligned_90_degrees_chk: started at 10ns failed at 35ns
Offending ‘((t2 - t1) == half_time_period)’

[nimitz_class]

In reply to ben@SystemVerilog.us:

I see this in my waveform. Please click on the link below to see the image

Your text to link here…

[nimitz_class]

In reply to nimitz_class:

After adding some tolerance to the property I’m able to make it pass. Thanks Ben :)

[suvendrakumarsahoo]

In reply to ben@SystemVerilog.us:

I want to measure two clock frequency with same phase

property phase_smps_pulse_check;
    realtime t1, t2;
    @(posedge tb_clk) (1, t1=$realtime) ##0 (top_adcdigen && top_adcanaen) |-> @(posedge top_smps_pulse) (1, t2=$realtime) ##0 ((t2-t1) >= (0+1fs));
  endproperty

assert property(phase_smps_pulse_check);

It is giving assertion error. What is wrong in it ?

Also I want to measure 180 degree out phase for two clock , what to change it in the code ?

I have added the stimulii in below link.

wave hosted at ImgBB — ImgBB