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.
- 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
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115