Clock Gating System Verilog Property assertion

Let say I have three signal : input clk_in , input rst_b, output clk_out. How can I get an assertion to check if clk_out is toggling only after 2 clk_in cycles after the rising edge of rst_b. The assertion should fails if the clk_out is delayed more/less than 2 cycles and the assertion should also fail when clk_out stop toggle before rst_b goes 0. When rst_b ==0, the clk_out should be 0 too.

I have tried this:
property_assert: assert property(@(posedge clk_in or negedge clk_in) $rose(rst_b) |-> ((##[0:3] clk_out == 0) and (##4 (clk_out==clk_in) throughout rst_b)));

However, it still passing the following waveform:

In reply to kinyau94:

  • From the way you described the requirements, it sounds like clk_out is a gated version of clk_in where gate is the enabling gate control.
  • When the gate s in the enabling mode, clk_out is exactly clk_in. Thus, sampling clk_out with posedge clk_in does not really sample the value clk_out after the edge of clk_in.
  • I fell more comfortable creating a delayed version clk_in by 1ns, and use that as the sampling clock for clk_out. I also feel more comfortable writing multiple assertions, and using tasks for complex assertions (see my paper on this topic at
    SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy

module top; 
        timeunit 1ns;     timeprecision 100ps;    
        logic clk_in=0, clk_ind1, clk_out, gate;
         
        default clocking @(posedge clk_in); 
        endclocking
        initial forever #10 clk_in=!clk_in;  
        assign #1 clk_ind1= clk_in; 
        
        // check if clk_out is toggling only after 2 clk_in cycles after the rising edge of gate.
        // The assertion should fails if the clk_out is delayed more/less than 2 cycles 
        // and the assertion should also fail when clk_out stop toggle before gate
        // goes 0. When rst_b ==0, the clk_out should be 0 too.
        
// Sampled at all cycles
        ap: assert property(@ (posedge clk_ind1) $fell(gate) |-> clk_out==1'b0); 
 
        // Used to compare clk_in and clk_out when gated ON. 
        task automatic t_gated_clks();
            while(gate!=0)  
              @(posedge clk_ind1 or negedge clk_ind1)
              assert(clk_out==clk_in); 
        endtask

        // Fire the gated comparison after rose(rose). 
        ap_rose_gate: assert property( @ (posedge clk_in)   
        $rose(gate) ##2 1'b1 |->  (1, t_gated_clks()) );        
        
         always begin // check 2 zero outs for 2 clk periods 
            wait($rose(gate));
            // fire once 
            ap_at_rose_gate: assert property(@(posedge clk_in)
             @(posedge clk_ind1) clk_out == 0 [*2]);

            ap_at_rose_gate2: assert property(@(posedge clk_in)
              @(negedge clk_ind1) clk_out == 0 [*2]);
        end
          

// Code was not tested, but this should help you with the concepts.

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


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy