How to write assertions for a Clock divider

SystemVerilog
3

In reply to yoshiko:

You can use the local variable in assertions and apply checks for consecutive rising edge and consecutive falling edge. For example : -
if you have to check div/VALUE , where VALUE=2 then you can write the following

property o_clk_even_rose_div(div_clk , n) ; 
 int local_cnte;
  @(posedge i_clk ) disable iff (~div_reset_check) 
($rose(div_clk[n]) ,local_cnte=0) |=> (1'b1,local_cnte=local_cnte+1)[*1:$] ##0 (local_cnte==VALUE/2) ##0 $fell(div_clk[n]);

endproperty

similarly you can write for the falling edge this will take care of your duty cycle.
In the case of odd division type
apply the assertion for posedge and the negedge and local_cnt will be equal to VALUE and not VALUE/2 in case of odd division.

PS:CHECK FOR SYNTAX

Prashant