Specifying Clock edge in the Consequent

SystemVerilog
,
1

Hi all ,

Generally while writing properties we mention the clock before antecedent


 property  ab ;
  @( posedge clk )  a  |=>  b  ;
 endproperty

I have observed properties where multiple clocks are specified in the property


 property  mclocks1 ;
  @( posedge clk0 )  a  |=>  @( posedge clk1 )  b  ;
 endproperty

 property  mclocks2 ;
  @( posedge clk0 )  c  |->  @( posedge clk1 )  d  ;
 endproperty

Above property ’ mclocks1 ’ looks for ’ a ’ being True at posedge of clk0 .

Then ’ b ’ Must be True at the Immediate Next posedge of clk1 ( following posedge clk0 ) .

Same goes for property ’ mclocks1 ’
i.e ’ d ’ Must be True at the Immediate Next posedge of clk1 following posedge of clk0

For Duty Cycle related assertions I observe the code as follows ::


  property check_Ton ;
        realtime current_time;
      
      @(posedge clk)  ( 1, current_time = $realtime  )  |=>  
      
        @(negedge clk)  ( ton_time == ( $realtime - current_time ) );  
      
    endproperty

My question is regarding the combination of |=> @( negedge clk )

Suppose I have Clock generation as ::


    bit  clk ;
    
   initial  forever  #5  clk =  ! clk ;

So Posedge of Clk Occurs at TIME : 5 , 15 , 25 , 35 etc whereas Negedge occurs at TIME : 10 , 20 , 30 , 40 etc .

Let us assume at TIME : 5 the property is evaluated . So current_time would be 5ns ( Assuming 1ns / 1ns )

So what does the combination of |=> @( negedge clk ) mean ?

[1] Does it wait for Next posedge of clk ( due to |=> ) i.e TIME : 15 and then wait for negedge of clk at TIME : 20 ?

[2] Also if I were to write |-> instead of |=> would it’s meaning change ?

2

In reply to hisingh:

|=> is equivalent to ##1 1 |-> 
//Thus, 
 @( posedge clk0 )  a  |=>  @( posedge clk1 )  b  ; 
// is equivalent to 
 @( posedge clk0 )  a  ##1 1 |->  @( posedge clk1 )  b  ;

Multiclocked properties can use the overlapping |-> or non-overlapping implication |=> operators to create a multiclocked property from an antecedent sequence and a consequent property. The |=> or the |-> operators synchronize the last expression of the antecedent clocked with the antecedent clock and the first elements of the consequent property being evaluated clocked with the consequent clock. The synchronization is the same as the one used with ##1 (for the |=>) and ##0 (for the |->) operators.

1102×824 201 KB

1102×824 201 KB

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) Amazon.com
  3. Papers:

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/

3

In reply to ben@SystemVerilog.us:

Thanks Ben ,

So to answer my questions

[1] Combination of |=> @( negedge clk ) means at the immediate Next negedge of clk at TIME : 10 ( following the initial posedge clk at TIME : 5 )

[2] Since the clock events :: posedge clk and negedge clk are Never True at Same time ::


  |=>  @( negedge clk )   is  Same   as  |->  @( negedge clk )



property check_Ton ;
        realtime current_time;
 
      @(posedge clk)  ( 1, current_time = $realtime  )  |=>  //  Using Non - Overlapping
 
        @(negedge clk)  ( ton_time == ( $realtime - current_time ) );  
 
    endproperty 

 //   Can  Also  be  Written  as 

 property check_Ton ;
        realtime current_time;
 
      @(posedge clk)  ( 1, current_time = $realtime  )  |->  //  Using Overlapping
 
        @(negedge clk)  ( ton_time == ( $realtime - current_time ) );  
 
    endproperty