Assertion for clock gating

SystemVerilog
1

Hi,

I want to write a pure assertion for clock gating. I am having ref_clk, p_clk, and clk_gate signals present in my assertion module.

  1. I want to write a seq/property-based assertion to check my clock dies within 50 clock cycles of ref_clk once the clk_gate is asserted.
  2. I also want to writeanother assertion to check if the clock is toggling after 50 clock cycles of clk_gate being de-asserted.

POV. I don’t want to use an always block.

2 
// Sequence to detect p_clk toggle edge
sequence p_clk_toggle;
  @(posedge ref_clk) $rose(p_clk) or $fell(p_clk);
endsequence

// 1) Check clock stops toggling within 50 ref_clk cycles after clk_gate asserted
property clock_die_within_50_cycles;
  @(posedge ref_clk)
  // When clk_gate asserted, then p_clk toggle stops within 50 cycles
  clk_gate |-> 
    (!p_clk_toggle)[*1:50];
endproperty

// 2) Check clock toggling after 50 ref_clk cycles of clk_gate de-asserted
property clock_toggle_after_50_cycles;
  @(posedge ref_clk)
  // clk_gate falls, then p_clk toggle appears at least once after 50 cycles
  (!clk_gate) |=> 
    ##[50:$] (p_clk_toggle);
endproperty

// Assertions instantiations
assert property (clock_die_within_50_cycles)
  else $error("p_clk did not stop toggling within 50 ref_clk cycles after clk_gate assertion");

assert property (clock_toggle_after_50_cycles)
  else $error("p_clk did not toggle after 50 ref_clk cycles of clk_gate de-assertion");