Clock Frequency Checker

I have tried the below code for checking the clock frequency.
This is always pass even if the frequency is not matched.
Can anyone please help me by suggesting what necessary corrections are needed?

Code:
time clock_input= 100ns;
property clk_freq;
time current_time;

@ (posedge clk)
disable iff ( !(!(reset) && (flag)))

('1, current_time = $time) |=> (clock_input <= ($time - (current_time-0.001ns))|| ($time - (current_time+0.001ns)));
endproperty

CLK_FREQ:assert property (clk_freq);

Thanks in advance.
Leya

In reply to leya:
I would use realtime and $realtime.
In my SVA Handbook I recommend the use of specific notations as they provide information about the use of the object. Am providing those guideline http://systemverilog.us/vf/notation_sv.pdf
You may disagree with my notation, and that is OK. Choose a notation that you feel comfortable with, but be consistent.


property p_clk_freq;
    realtime current_time;
    @ (posedge clk)
    disable iff ( !(!(reset) && (flag)))
        ('1, current_time = $realtime) |=> 
        (clock_input <= ($realtime - (current_time-0.001ns))|| ($time - (current_time+0.001ns)));
endproperty
  
ap_clk_freq: assert property (clk_freq);

// Old code on clock frequency check I wrote 
	property p_clk_hi; 
	  realtime v; 
	  @(posedge clk) (1, v=$realtime) |-> @(negedge clk) ($realtime-v)==300ns;
	endproperty 
	ap_clk_hi: assert property(p_clk_hi);  
		
	property p_clk_lo; 
	  realtime v; 
	  @(negedge clk) (1, v=$time) |-> @(posedge clk) ($realtime-v)==700ns;
	endproperty 
    ap_clk_lo: assert property(p_clk_lo);  
 

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


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

In reply to ben@SystemVerilog.us:
To test your code, you may want to use a modified approach similar to the shown below where I introduce random jitter in the clock. This is a quick way to verify your assertion.


import uvm_pkg::*; `include "uvm_macros.svh" 
module m; 
	bit clk=1, a;  
	bit[0:1] t; 
	default clocking @(posedge clk); endclocking
	initial forever begin 
	   #298 if (!randomize(t)  with 
           { t dist {1'b1:=1, 1'b0:=10};
           }) `uvm_error("MYERR", "This is a randomize error")
       if(t) begin 
          clk=!clk;
	      #1ns clk=!clk;
	      #1ns clk=!clk; 
	     end 
	   else #2ns clk=!clk; 
	   #398  if (!randomize(t)  with 
           { t dist {1'b1:=1, 1'b0:=10};
           }) `uvm_error("MYERR", "This is a randomize error")
       if(t) begin 
          clk=!clk;
	      #1ns clk=!clk;
	      #1ns; 
	      end 
	   else #2ns;   
	   #300  clk=!clk;	
	 end 

	property p_clk_hi; 
	  realtime v; 
	  @(posedge clk) (1, v=$realtime) |-> @(negedge clk) ($realtime-v)==300ns;
	endproperty 
	ap_clk_hi: assert property(p_clk_hi);  
		
	property p_clk_lo; 
	  realtime v; 
	  @(negedge clk) (1, v=$time) |-> @(posedge clk) ($realtime-v)==700ns;
	endproperty 
    ap_clk_lo: assert property(p_clk_lo);  
endmodule   

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


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

In reply to ben@SystemVerilog.us:

Hi Ben,
Thank you for the input.
I have tried to change the value of clock_input.
Still the assertion is passing.
Can you suggest any changes?

property p_clk_freq;
realtime current_time;
@ (posedge clk)
disable iff ( !(!(reset) && (flag)))
('1, current_time = $realtime) |=>
(clock_input <= ($realtime - (current_time-0.001ns))|| ($time - (current_time+0.001ns)));
endproperty

ap_clk_freq: assert property (clk_freq);

Thanks,
Leya

In reply to ben@SystemVerilog.us:

Hi Ben,
Thank you for the input.
I have tried to change the value of clock_input.
Still the assertion is passing.
Can you suggest any changes?

property p_clk_freq;
realtime current_time;
@ (posedge clk)
disable iff ( !(!(reset) && (flag)))
('1, current_time = $realtime) |=>
(clock_input <= ($realtime - (current_time-0.001ns))|| ($time - (current_time+0.001ns)));
endproperty

ap_clk_freq: assert property (clk_freq);

Thanks,
Leya

In reply to leya:
Apologies for my mistake, as the comparison expression I used is incorrect.
What you need, and really mean, is inside a region.

 1800: 11.4.13 Set membership operator
 inside_expression ::= expression  inside  { open_range_list }
 int a, b, c;
if ( a inside {b, c} ) ...
// THUS, 
property p_clk_freq;
            realtime current_time;
            @ (posedge clk)
            disable iff ( !(!(reset) && (flag)))
            ('1, current_time = $realtime) |=> 
           // (clock_input <= ($realtime - (current_time-0.001ns))|| 
           //                 ($realtime - (current_time+0.001ns)));
            ($realtime - current_time) inside {clock_input - 0.001ns, clock_input + 0.001ns}  
        endproperty
        ap_clk_freq: assert property (p_clk_freq); 

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


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

In reply to ben@SystemVerilog.us:

Hi Ben,

Thank you for the new code.
Tried this,but now getting fail.
Maybe ,if I could display the values ,then could analyse the fail.
Is there a way to display the value for ($realtime - current_time))?
Any other approach possible?

Thanks,
Leya

In reply to leya:
OK, the following works, I had 26 passes and 3 failures.

 
property p_clk_freq2;
            realtime current_time;
            @ (posedge clk)
            // disable iff ( !(!(reset) && (flag)))
            ('1, current_time = $realtime) |=> (1, $display ("p=%t", $realtime - current_time))
           // (clk_period <= ($realtime - (current_time-0.001ns))|| 
           //                 ($realtime - (current_time+0.001ns)));
            // 11.4.13 Set membership operator
            // inside_expression ::= expression inside { open_range_list }
            //int a, b, c;
            // if ( a inside {b, c} ) ...
            ##0  ($realtime - current_time) <= clk_period + 1ns and 
            ($realtime - current_time) >= clk_period - 1ns; 
        endproperty
        ap_clk_freq2: assert property (p_clk_freq2);

I have to analyze why the solution with the inside fails.
Below is my Testbench code.


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
    timeunit 1ns;     timeprecision 100ps;    
    bit clk, clk2, a, b;
    realtime clk_period= 20ns;  
	default clocking @(posedge clk); endclocking
        initial forever #(clk_period/2 + a*1ns -b*1ns) clk=!clk;  
        initial forever  #10ns clk2=!clk2;  
        initial begin
            $timeformat(-9, 1, "ns", 8);
            $display("%t", $realtime);
        end 
        
        property p_clk_freq;
            realtime current_time;
            @ (posedge clk)
            // disable iff ( !(!(reset) && (flag)))
            ('1, current_time = $realtime) |=> 
           // (clk_period <= ($realtime - (current_time-0.001ns))|| 
           //                 ($realtime - (current_time+0.001ns)));
            // 11.4.13 Set membership operator
            // inside_expression ::= expression inside { open_range_list }
            //int a, b, c;
            // if ( a inside {b, c} ) ...
            ($realtime - current_time) inside {clk_period - 0.2ns, clk_period + 0.2ns}  
        endproperty
        ap_clk_freq: assert property (p_clk_freq);

        property p_clk_freq2;
            realtime current_time;
            @ (posedge clk)
            // disable iff ( !(!(reset) && (flag)))
            ('1, current_time = $realtime) |=> (1, $display ("p=%t", $realtime - current_time))
           // (clk_period <= ($realtime - (current_time-0.001ns))|| 
           //                 ($realtime - (current_time+0.001ns)));
            // 11.4.13 Set membership operator
            // inside_expression ::= expression inside { open_range_list }
            //int a, b, c;
            // if ( a inside {b, c} ) ...
            ##0  ($realtime - current_time) <= clk_period + 1ns and 
            ($realtime - current_time) >= clk_period - 1ns; 
        endproperty
        ap_clk_freq2: assert property (p_clk_freq2);
        
        initial begin 
            bit va, vb; 
            repeat(200) begin 
                @(posedge clk);   
                if (!randomize(va, vb)  with 
                { va dist {1'b1:=1, 1'b0:=3};
                vb dist {1'b1:=1, 1'b0:=3};      
            }) `uvm_error("MYERR", "This is a randomize error")
            a <= va; 
            b <= vb;
        end 
        $stop; 
    end 
endmodule    

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


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

In reply to ben@SystemVerilog.us:
1800 says that The expression on the left-hand side of the inside operator is any singular expression.
It looks like the inside does not work on real or realtime types.
The use of comparison operators is thus best suited.


 property p_clk_freq2;
            realtime current_time;
            @ (posedge clk)
            disable iff ( !(!(reset) && (flag)))
            ('1, current_time = $realtime) |=> (1, $display ("p=%t", $realtime - current_time))
            ##0  ($realtime - current_time) <= clk_period + 1ns and // sequence and
            ($realtime - current_time) >= clk_period - 1ns; 
        endproperty
        ap_clk_freq2: assert property (p_clk_freq2); 

// ALSO OK 
property p_clk_freq3;
            realtime current_time;
            @ (posedge clk)
            disable iff ( !(!(reset) && (flag)))
            ('1, current_time = $realtime) |=> (1, $display ("p=%t", $realtime - current_time))
            ##0 (($realtime - current_time) <= clk_period + 1ns && // logical and
                 ($realtime - current_time) >= clk_period - 1ns); 
        endproperty
        ap_clk_freq3: assert property (p_clk_freq3);

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


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

In reply to ben@SystemVerilog.us:

Hi Ben,

Thank you very much for the above code.
I have tried it.Its working fine.

Thanks,
Leya

Why is '1 required in SV assertion while checking frequency?

In reply to Sagar Wakle:


      realtime current_time;
      @ (posedge clk)
            disable iff ( !(!(reset) && (flag)))
            ('1, current_time = $realtime) |=> ...

// From 1800'2017 a sequence can be defined as 
sequence_expr ::=
...
| ( sequence_expr {, sequence_match_item} ) [ sequence_abbrev ]

sequence_match_item ::=
  operator_assignment
  | inc_or_dec_expression
  | subroutine_call
// Example: At end of subsequence a ##1 b, j=0.
// Starting from next cycle c must remain 1 for as
// many cycles as defined by the value of the
// argument cy (j is incremented until j==cy).
property P(int cy);
  int j=0; // initialization optional, legal in SV’09
  (a ##1 b, j=0)|=> (c, j+= 1) [*0:$] ##1 j==cy;
endproperty : P

// In our case, we're checking for clock periods, and need at all clocking event  
// to set the local variable  current_time, thus we need to use the sequence definition 
// that includes a sequence_matched_item, i.e., 
// ( sequence_expr {, sequence_match_item} )
// Since we do that at every clocking event, our sequence_expr is true (a '1) 

Thanks Ben, its clear to me.