Assertion on clock gating

SystemVerilog
,
1

Hi,
I am trying to write assertion to check clock gating feature.

Whenever my clk_gate_cfg is 0 my clk will stop after 2:3 cycle for the particular block and will remain stop/zero till clk_gate_cfg will not assert.

Like in my env i have reg “clk_gate_cfg” .It has 8 bit register.

I have wrote below assertion for the above requirement. Please let me know where i am doing wrong.
This assertion is passing in every cases.

property clk_gating
@(posedge top_th.ref_clk)
((top_th.abc.abc_core.cfg_reg.clk_gate_cfg[1] == 0) ##[2:3]  (!top_th.abc.abc_core.trif_core[1].clk_i)) |->  top_th.abc.abc_core.trif_core[1].clk_i ==0 throughout (top_th.abc.abc_core.cfg_reg.clk_gate_cfg[1]==1)[->1]
endproperty
2

In reply to kuldeep sharma:
I see your requirements as:


//Whenever my clk_gate_cfg is 0 my clk will stop after 2:3 cycle 
// for the particular block and will remain stop/zero till clk_gate_cfg will not assert.

// Like in my env i have reg "clk_gate_cfg" .It has 8 bit register.
property clk_gating
@(posedge top_th.ref_clk)
  $fell(top_th.abc.abc_core.cfg_reg.clk_gate_cfg[1]) |->   
  ##[2:3] top_th.abc.abc_core.trif_core[1].clk_i ==0 [*1:$] intersect 
                (top_th.abc.abc_core.cfg_reg.clk_gate_cfg[1]==1)[->1];
endproperty

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
3

In reply to ben@SystemVerilog.us:

Hi Ben,

Thanks for the reply. I have few queries.

How many times Assertion print will come ?
Or Will it come when "clk_gate_cfg[1]==1) ?
Above assertion is not failing when i am doing clock disable for fist bit and checking clock for another block .In my desgin 1 bit is gating clock for 1 instance of core. Like

property clk_gating
@(posedge top_th.ref_clk)
fell(top_th.abc.abc_core.cfg_reg.clk_gate_cfg[1]) |-> ##[2:3] top_th.abc.abc_core.trif_core[2].clk_i ==0 [*1:] intersect
(top_th.abc.abc_core.cfg_reg.clk_gate_cfg[1]==1)[->1];
endproperty

4

In reply to kuldeep sharma:
I went overboard on the use of the intersect


 // !a[*1:$] intersect a[->1] should fail
 // !a[*1:$] ##1 a intersect a[->1] // ok
  // but then you don't need the intersect 
$fell(top_th.abc.abc_core.cfg_reg.clk_gate_cfg[1]) |->   
  ##[2:3] top_th.abc.abc_core.trif_core[1].clk_i ==0 [*1:$] ##1
                (top_th.abc.abc_core.cfg_reg.clk_gate_cfg[1];

Clarify your comments

5

In reply to ben@SystemVerilog.us:

Am not reading the requirements correctly, but you get the ideas of options.
Hopefully it’s a guide
BTW, in the consequent you should consider it first_match.

first_match(##[1 ;2] b)##1 c

6

You could also implement a cntr on the clk you are trying to check and then check something like this in your assertion : cntr==$past(cntr)

7

Hi @ben2
What this represent in your code"[->1]"

property clk_gating
@(posedge top_th.ref_clk)
  $fell(top_th.abc.abc_core.cfg_reg.clk_gate_cfg[1]) |->   
  ##[2:3] top_th.abc.abc_core.trif_core[1].clk_i ==0 [*1:$] intersect 
                (top_th.abc.abc_core.cfg_reg.clk_gate_cfg[1]==1)[->1];
endproperty
8

a[->1] is equivalent to !a[*0:$] ##1 a

9

a[->1] is equivalent to !a[*0:$] ##1 a