SV assertion for clock gating & Reset check

In reply to S.P.Rajkumar.V:

Assumption: g_clk takes few cycles time before it really gets gated (corresponds to [2:4] below)

property clk_gating_check_g_clk;
@posedge(ref_clk)
($fell(clk_en) ##[2:4] ~g_clk) |-> (~g_clk throughout clk_en[->1]);
endproperty

At first glance, it looked to me like you need a first_match() in the antecedent, as you have multiple possible matches, and all threads of the antecedent must be tested and must succeed.
However, after more thoughts, you do NOT want the first_match() in this particular case.

I recommend that you modify your not operator to the bitwise negative operator. Thus,

	property clk_gating_check_g_clk;
		@(posedge ref_clk)
			($fell(clk_en) ##[2:4] !g_clk) |-> (!g_clk throughout clk_en[->1]);
	endproperty		
    ap_clk_gating_check_g_clk: assert property(clk_gating_check_g_clk);

Rationale: Since your variable are declared as single bits, you should use good coding practices, and use the Binary logical operators instead of the Binary bitwise operators. You are doing logical operations.
Yes, you get the same result in either case, but the notion is different.

  1. On the similar lines, I have written a property for reset as well. This is resulting in false assertion failure at reset release; as the disabling of res_en and release of reset happens at the same time in design, where-as throughout expects it to happen after a cycle delay. Need help to get it resolved.
    Reset enable: res_en
    Reset signal: reset_n
    clock: ref_clk
property rst_chk_enbl;
@(posedge ref_clk)
$rose(res_en) |-> (~reset_n throughout res_en [->0]);
endproperty

Thanks,

[list=1]
[*] The goto with 0 does not make sense: [->0]
b [->m] is equivalent to ( !b [*0:$] ##1 b)[*m], thus
(~reset_n throughout res_en [->0]) is same as
(~reset_n throughout res_en [0])
[
] You probably meant

property rst_chk_enbl;
  @(posedge ref_clk)
    $rose(res_en) |-> (!reset_n throughout !res_en [->1]);
endproperty

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us