Verify the frequency of a clock

clock with 50% duty cycle and 1 MHz frequency

property p_clk_hi; 
      time v; 
      @(posedge clk) (1, v=$time) |-> @(negedge clk) ($time-v)==500ns;
    endproperty 
    ap_clk_hi: assert property(p_clk_hi);  

property p_clk_lo; 
  time v; 
  @(negedge clk) (1, v=$time) |-> @(posedge clk) ($time-v)==500ns;
endproperty 
ap_clk_lo: assert property(p_clk_lo);

why there are using “1” in assertion?

In reply to anvesh dangeti:

Hello so basically whatever you find at the right of that one is known as sequence match item instead the 1 is known as sequence expr. So basically let’s rewrite the code:

Let’s use the activate input (it can be declared as bit activate as variable inside your property.

property p_clk_hi(activate); 
      time v; 
      @(posedge clk) (activate, v=$time) |-> @(negedge clk) ($time-v)==500ns;
endproperty

ap_clk_hi: assert property(p_clk_hi(0));

This means that you could easily create a customized property using freq variable and function that would help you computing the period or semi one.
You can easily replace the (activate,fcall) as if(activate==1) then call facll. Do not call fcall is 0

In reply to anvesh dangeti:

“antecedent” |-> “consequent”

  • The left-hand side of the implication is called the “antecedent” and the right-hand side is called the “consequent”.
  • The antecedent is the gating condition.
  • If the antecedent succeeds, then the consequent is evaluated.

property p_clk_hi; 
      time v; 
      @(posedge clk) (1, v=$time) |-> @(negedge clk) ($time-v)==500ns;
endproperty
//here to make the antecedent succeed or evaluated to be true at each posedge clk,
//'1' is added there. Now antecedent is always TRUE, and time is captured at each 
//posedge of clk and consequent is evaluated and time difference is checked