SV assertion for clock gating & Reset check

SystemVerilog
12

In reply to S.P.Rajkumar.V:

In reply to S.P.Rajkumar.V:

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

After little more analysis, I believe initial assertion would work fine even in the case reported by you (i.e, g_clk being gated version of ref_clk).
Because, ‘throughout’ as the name suggests that, it checks for validity of some condition (!g_clk) as long as other condition (CLK_EN → 1) becomes true; It doesn’t check only at each posedge of ref_clk_i.

Wrong on the following statement: It doesn’t check only at each posedge of ref_clk_i.
with

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

All variables ARE SAMPLED @(posedge ref_clk)
This would solved the problem though by using a multiclock, specifically,
@(negedge ref_clk) in the consequent.

@(posedge ref_clk)
    ($fell(clk_en) ##[2:4] !g_clk) |-> 
              @(negedge ref_clk)(!g_clk throughout clk_en[->1]);

BTW, g_clk is sampled in the Preponed region, thus, with clk_en==1’b1, @posedge(ref_clk) the sampled value of g_clk==0 (it has not risen yet).
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us