Assertion for this feature

SystemVerilog
,
1

Hi
I need help in this assertion for this design requirement .
Design Requirement :
There are two signals ,clk_en and clk_gated(491Mhz) ,clk_ref(983Mhz)
WHen “clk_en” is toggled from 0->1 , the clk_gated(491MHz) starts toggling after a delay of 5 clk cycles of clk_ref(983Mhz) .
And similarly when “clk_en” is toggled from 1 → 0 , the clk_gated stops toggling after a delay of 8clk cycles of clk_ref .

I was to write an assertion for this , where we check is clk is toggling after a specific number of cycles and it is continuously toggling when clk_en is 1 and stops toggling when clk_en is zero .

I have done in this way , can you please help what else is missing in this assertion :

property enable_clk_gated_prop_1(logic en, logic clk_ref, logic clk_gated, logic clk_en);
@(posedge clk_ref) disable iff (!en)
(clk_en && $past(clk_en,5)) |-> (clk_gated != $past(clk_gated));
endproperty

property disable_clk_gated_prop_1(logic en, logic clk_ref, logic clk_gated, logic clk_en );
@(posedge clk_ref) disable iff (!en)
(!clk_en && !$past(clk_en,10)) |-> (clk_gated == $past(clk_gated));
endproperty

2

I’ll explain the process at

  1. Understanding the requirements an implications.
  2. Arriving at the assertions.

Requirements: I submit the requirements to AI (I use perplexity.ai or x.ai) so as to explore implications, what is not said, and possible ideas I am missing.
https://www.perplexity.ai/search/with-these-requirements-for-an-Exo2Tu9AQhKyefEtvVDtIA

  1. Getting to the assertions. In this case, refclk is 2x the gated clk.
    For complex assertions, I often start with tasks started by the detection of an attempted event.
bit  clk, clk_ref, clk_gated, en=1;
  int pass0, pass1, err0, err1, tbcount0, tbcount1; 
  always #50ps clk_ref=!clk_ref; 
  always @(posedge clk_ref) clk<=!clk; 

// THIS IS A CONCEPT, IT NEEDS TUNING!!!!!
// FORK OF A TIMEOUT AND A COUNT OF ACTIVE CLOCKS
// THEN TEST THE NUMBER OF ACTIVE CLOCKS AGAINST EXPECTED RANGE
task automatic t_clk_en0();
       int count; 
       fork  
        #5.1ns ; // 5 clks
         forever @(posedge clk_gated) if(!en) begin 
            count=count+1;
            tbcount0=count; // debbug
         end 
       join_any
      am_3clk_after_en: assert(count < 5) pass0++; else err0=err0+1;
    endtask
    // fire the task 
    // cover property(@(posedge clk_tb) !en |-> (1, t_clk_en0()));
    always @(negedge(en)) t_clk_en0(); 

// From there use a similar process with SVA
// Using the tb clock 
    property p_noclk_en; // adjust the max count allowed 
      int count=0; 
      @(posedge clk_ref) $fell(en) |-> ##1  
         ((1, count=count+clk)[*1:$]  intersect  $rose(en)[->1]) ##0 count<8 ;
    endproperty
    ap_noclk_en: assert property(p_noclk_en) else err1=err1+1;  
====
// complete ode that needs tuning
module  switch;
  timeunit 1ns;  timeprecision 100ps;    
  bit  clk, clk_ref, clk_gated, en=1;
  int pass0, pass1, err0, err1, tbcount0, tbcount1; 
  always #50ps clk_ref=!clk_ref; 
  always @(posedge clk_ref) clk<=!clk; 
  
  always @(clk_ref) begin    // gated clk generation
    bit v_enb;
    case ({v_enb, en})
       2'b00: clk_gated=0; 
       2'b01:  begin 
           for (int i = 0; i<=7;i++ ) begin
            clk_gated=0; 
           end  // to clk after 8 clk_ref
           clk_gated=clk;
        end
       2'b10: begin // disable after 5
           for (int i = 0; i<=5;i++ ) begin
            clk_gated=clk; 
           end  // to clk after 8 clk_ref
           clk_gated=0;
        end
       2'b11: begin 
           v_enb=1; 
           clk_gated=clk;
       end
    endcase
  end 

    task automatic t_clk_en0();
       int count; 
       fork
        #5.1ns ; // 5 clks
         forever @(posedge clk_gated) if(!en) begin 
            count=count+1;
            tbcount0=count; // debbug
         end 
       join_any
      am_3clk_after_en: assert(count < 5) pass0++; else err0=err0+1;
    endtask
    // fire the task 
    // cover property(@(posedge clk_tb) !en |-> (1, t_clk_en0()));
    always @(negedge(en)) t_clk_en0(); 

    task automatic t_clk_en1();
       int count; 
       fork
        #5.1ns ; // 5 clks
         forever @(posedge clk_gated) if(en) begin 
            count=count+1;
            tbcount1=count; // debbug
         end 
       join_any
      am_5clk_after_en: assert(count < 8) pass1++; else err1=err1+1;
    endtask
    // fire the task 
    // cover property(@(posedge clk_tb) !en |-> (1, t_clk_en0()));
    always @(posedge(en)) t_clk_en1(); 

   // Using the tb clock 
    property p_noclk_en; // adjust the max count allowed 
      int count=0; 
      @(posedge clk_ref) $fell(en) |-> ##1  
         ((1, count=count+clk)[*1:$]  intersect  $rose(en)[->1]) ##0 count<8 ;
    endproperty
    ap_noclk_en: assert property(p_noclk_en) else err1=err1+1;  

    
    initial begin 
      $dumpfile("dump.vcd"); $dumpvars;
      repeat(5) @(posedge clk_ref);
      en <=0;
      repeat(10) @(posedge clk_ref);
      en <= 1; 
      repeat(20) @(posedge clk_ref);
      #30; $finish();
    end
endmodule