SVA to check frequency and duty cycle with +/- 5% error

SystemVerilog
, , , ,
1

Hi,

Is it legal to use multiple overlapping and non-overlapping operators in one sequence? I did not get any error because the antecedent did not satisfy, also can someone please help in getting this assertion correct?


module pll;
logic clk = 0;

property freq_chk_tol (logic clk, real tolerance, time duty_cycle);
     time current_time;
    @(posedge clk) (1, current_time=$time) |-> @(negedge clk) ($time-current_time)== 100ns |=> @(negedge clk) (1,current_time=$time) |-> @(posedge clk) ($time-current_time) == 100ns |=> @(posedge clk) ('1, current_time = $time) |-> @(negedge clk) (($time - current_time) >= (duty_cycle *(1 + tolerance/100.00)) && ($time - current_time) <= (duty_cycle *(1 - tolerance/100.00))) |=> @ (negedge clk) ('1, current_time = $time) |-> @(posedge clk) (($time - current_time) >= (duty_cycle *(1 + tolerance/100.00)) && ($time - current_time) <= (duty_cycle *(1 - tolerance/100.00))) ;
    endproperty : freq_chk_tol
    
  pll_chk: assert property (freq_chk_tol(clk, 5, 50));
  
  always
    begin
    clk = 1'b1;
    #20;
    clk = 1'b0;
    #80;
  end
  
  initial begin
    #50000 $finish;
  end
  
  endmodule

This assertion should have failed because the duty cycle of the clock generated is 20% and I’m trying to make it fail by passing 50% as duty cycle in the arguments. I know it’s not correct, please help!

Thanks

2

In reply to foxtrot:
You need to really understand the concept of vacuity. In general, there is very little need of properties with multiple implication operators; they are frown upon by experts.
Also, use smaller multiple assertions. See my other comment below the code.


module pll;
    logic clk = 0;
    
    property p_freq_chk_tol (int tolerance, realtime half_duty_cycle);
        realtime current_time;
        @(posedge clk) (1, current_time=$realtime) |-> 
        @(negedge clk) ($realtime-current_time) >= half_duty_cycle - (half_duty_cycle * tolerance)/100.0 && 
                       ($realtime-current_time) <= half_duty_cycle + (half_duty_cycle * tolerance)/100.0 ;
    endproperty : p_freq_chk_tol

    property p_freq_chk_to0 (int tolerance, realtime half_duty_cycle);
        realtime current_time;
        @(negedge clk) (1, current_time=$time) |-> 
        @(posedge clk) ($realtime-current_time) >= half_duty_cycle - (half_duty_cycle * tolerance)/100.0 && 
                         ($realtime-current_time) <= half_duty_cycle + (half_duty_cycle * tolerance)/100.0 ;
    endproperty : p_freq_chk_to0

    
    ap_freq_chk_tol : assert property (p_freq_chk_tol(5, 50ns));
    ap_freq_chk_to0 : assert property (p_freq_chk_to0(5, 50ns));
     
      always
        begin
        clk = 1'b1;  
        #20;
        clk = 1'b0;
        #80;
      end
     
      initial begin
        #50000 $finish;
      end
endmodule

I strongly suggest that you carefully read my paper
Understanding the SVA Engine
Verification Horizons
In it I used three different types of SVA properties are used to
emphasize different important concepts of SVA:

  1. Antecedent/consequent: This model demonstrates the concepts of spawned threads,
    leading clocking event, attempts.
  2. Range delays in the consequent: This model demonstrates the testing of each element of the
    range until success is reached and the lack of need to limit the ranges to a matched (i.e., valid) consequent.
  3. Range delays in the antecedent: This model demonstrates the testing of each element of the
    range and the need for a first_match operator or other technique to limit the ranges to a matched antecedent.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** 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:
3

In reply to ben@SystemVerilog.us:
Thanks, Ben. Will check it out :)

4

In reply to ben@SystemVerilog.us:

In reply to foxtrot:
You need to really understand the concept of vacuity. In general, there is very little need of properties with multiple implication operators; they are frown upon by experts.
Also, use smaller multiple assertions. See my other comment below the code.
Edit code - EDA Playground


module pll;
logic clk = 0;
property p_freq_chk_tol (int tolerance, realtime half_duty_cycle);
realtime current_time;
@(posedge clk) (1, current_time=$realtime) |-> 
@(negedge clk) ($realtime-current_time) >= half_duty_cycle - (half_duty_cycle * tolerance)/100.0 && 
($realtime-current_time) <= half_duty_cycle + (half_duty_cycle * tolerance)/100.0 ;
endproperty : p_freq_chk_tol
property p_freq_chk_to0 (int tolerance, realtime half_duty_cycle);
realtime current_time;
@(negedge clk) (1, current_time=$time) |-> 
@(posedge clk) ($realtime-current_time) >= half_duty_cycle - (half_duty_cycle * tolerance)/100.0 && 
($realtime-current_time) <= half_duty_cycle + (half_duty_cycle * tolerance)/100.0 ;
endproperty : p_freq_chk_to0
ap_freq_chk_tol : assert property (p_freq_chk_tol(5, 50ns));
ap_freq_chk_to0 : assert property (p_freq_chk_to0(5, 50ns));
always
begin
clk = 1'b1;  
#20;
clk = 1'b0;
#80;
end
initial begin
#50000 $finish;
end
endmodule

I strongly suggest that you carefully read my paper
Understanding the SVA Engine
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
In it I used three different types of SVA properties are used to
emphasize different important concepts of SVA:

  1. Antecedent/consequent: This model demonstrates the concepts of spawned threads,
    leading clocking event, attempts.
  2. Range delays in the consequent: This model demonstrates the testing of each element of the
    range until success is reached and the lack of need to limit the ranges to a matched (i.e., valid) consequent.
  3. Range delays in the antecedent: This model demonstrates the testing of each element of the
    range and the need for a first_match operator or other technique to limit the ranges to a matched antecedent.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** 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:

Is there a way to combine both properties into one? use of non-overlapping is not working


property p_freq_chk_tol (int tolerance, realtime half_duty_cycle);
        realtime current_time;
        disable iff (rst)
        @(posedge clk) (1, current_time=$realtime) |-> 
        @(negedge clk) ($realtime-current_time) >= half_duty_cycle - (half_duty_cycle * tolerance)/100.0 && 
                       ($realtime-current_time) <= half_duty_cycle + (half_duty_cycle * tolerance)/100.0 |=> /*use of non-overlapping here is correct?*/@(negedge clk) (1, current_time=$time) |->
        @(posedge clk) ($realtime-current_time) >= half_duty_cycle - (half_duty_cycle * tolerance)/100.0 && 
                         ($realtime-current_time) <= half_duty_cycle + (half_duty_cycle * tolerance)/100.0;
    endproperty : p_freq_chk_tol