Assertion not firing at neg edge of clock

[Alex_Verif]

//GatedCLK is gating clock. 
 property ClockGATING_dis_check_p (bit ref_clk, bit GatedCLK, bit clk_ENable);
    @(posedge ref_clk)
     $rose(clk_ENable)  |-> ##[A:B]  ( GatedCLK === ref_clk throughout clk_ENable[->0])  ;
 endproperty;

 sequence clk_gated_sequence;
      @(posedge ref_clk) $fell(clk_ENable) ;
 endsequence;



 property ClockGATING_enabled_check_p (bit ref_clk, bit GatedCLK, bit clk_ENable);
    @(posedge ref_clk) 
   ( clk_gated_sequence  |-> ##[A:B]  ( GatedCLK === 0 throughout clk_ENable[->1] )       );
 endproperty;

Questions:

1. What is the better way to check if gated-clock is running or not (when clock enable is high).
2. I dont see “ClockGATING_enabled_check_p” property firing when clk_ENable falls RATHER it fires at rising edge of clk_ENable.

[ben2]

In reply to Alex_Verif:
The issue here is that from the ref_clk, you drive a clk_enable from a FF, thus with some sort of hold time. Then, this clk_enble is gated with ref_clk to get a gated_clk, adding another gate delay. Thus, everything is not run from a single clock. The best approach is to use tasks, as described in my paper at:
SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
The test code is at http://systemverilog.us/vf/gated_clk2.sv
Key portions of the code:

bit ref_clk, GatedCLK, clk_ENable;  
    initial forever #10ref_clk=!ref_clk;   
    let HOLD_TIME=2ns;
    always @ (*) begin
        if(clk_ENable) #1 GatedCLK=ref_clk; 
        else #1 GatedCLK=1'b0; 
    end  

    task automatic check_gated_hi();
        while (clk_ENable) begin
            #HOLD_TIME; 
            a_REF_HI: assert (GatedCLK == ref_clk); 
            @(negedge ref_clk); 
            #HOLD_TIME; 
            a_REF_LOW: assert (GatedCLK == ref_clk); 
        end
    endtask 

    task automatic check_gated_lo();
        while (clk_ENable) begin
            #HOLD_TIME; 
            a_REF_HI0: assert (GatedCLK == 1'b0); 
            @(negedge ref_clk); 
            #HOLD_TIME; 
            a_REF_LOW0: assert (GatedCLK == 1'b0); 
        end
    endtask 
    
    ap_clk_enb_HI: assert property(@ (posedge ref_clk) 
       $rose(clk_ENable)  |-> (1, check_gated_hi()) ); 
       
    ap_clk_enb_LO: assert property(@ (posedge ref_clk) 
       $fell(clk_ENable)  |-> (1, check_gated_lo()) );  

Simulation results: http://systemverilog.us/vf/gated_clock.png

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. SVA Alternative for Complex Assertions
   https://verificationacademy.com/news/verification-horizons-march-2018-issue
2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
3. 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

[ben2]

In reply to ben@SystemVerilog.us:

One more thing, if the clock_enable is triggered from a negedge, the glitch due to hold times goes away.

// Testbench code 
   @(negedge ref_clk);  #1; 
            if (!randomize(clk_ENable)  with 
            { clk_ENable dist {1'b1:=2, 1'b0:=1};            
        }) `uvm_error("MYERR", "This is a randomize error") 

http://systemverilog.us/vf/gated_clk3.sv

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. SVA Alternative for Complex Assertions
   https://verificationacademy.com/news/verification-horizons-march-2018-issue
2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
3. 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