Assertion : ClkGate state and TransactionCount assertion

SystemVerilog
,
1

FSMstate goes to Clkgate state and clk will be gated when TransCnt=0 after some 0-10 clock cycle
FSM state ungates the clk when TransCnt!=0 after some 0-10 clk cycles
ClkGateState=2
Idle=0
I need to write some assertions for that
1.


//Check when TransCnt=0, Clock will be Gated till TransCnt!=0
   property assert1(bit reset);
   @(negedge TBclk) disable iff(!reset) 
   (TranCnt==0) |-> ##[0:10] (Clk == 0) throughout (~(TransCnt==0)[->1])); 
 endproperty
  Worked for me

2. //Check when State=Gatedstate, TransCnt=0
   property assert2(bit reset);
   @(negedge TBclk) disable iff(!reset) 
   (State==2)[*10] |-> (TransCnt==0) 
 endproperty
 

   This is not working , 
   Once TransCnt=0, after some 10 clock cycles, State =2. From here Assertion triggers and Passes.
   When TransCnt=1, after some 10 clock cycles State will be zero. -> ASSERTION FAILS HERE as State is takign some 10 clks to go to IDLE.

Can someone help me to work on 2nd assertion
So Assertion is failing at

2

In reply to naaj_ila:
I don’t understand the issue.
Maybe you need a $rose(State==2)

3

In reply to ben@SystemVerilog.us:

I want to write an assertion similarly like this
1.When Clk is Gated(state=2) , i want to make sure TransCnt=0.
Note:: when TransCnt!=0, Clk will be Ungated within 0 to 10 clkcycles.

property clkgate_state_p(bit reset);
   @(negedge TBCLK) disable iff(!reset) 
   (State_ps == 2)  |-> $past((TransCnt==0),[0:10]);  
 endproperty

I want to make sure TransCnt=0 when State=2. TransCnt will be zero before some 0-10 clk cycles.
Similarly like above assertion

4

In reply to naaj_ila:


// $past(rnge) is illegal Illegal 
 (State_ps == 2)  |-> $past((TransCnt==0),[0:10]);  

// However, you can use the endpoints (.triggered) of a sequence. Thus, 
// UPDATED SOLUTION IN MY LAST POST BELOW

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** 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:
  1. Papers:
    Understanding the SVA Engine,
    Verification Horizons - July 2020 | Verification Academy
    Reflections on Users’ Experiences with SVA, part 1
    Reflections on Users’ Experiences with SVA | Verification Horizons - March 2022 | Verification Academy
    Reflections on Users’ Experiences with SVA, part 2
    Reflections on Users’ Experiences with SVA, Part II | Verification Horizons - July 2022 | Verification Academy
    SUPPORT LOGIC AND THE ALWAYS PROPERTY
    http://systemverilog.us/vf/support_logic_always.pdf
    SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
    SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
    SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
    https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.
    Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
    https://www.udemy.com/course/sva-basic/
    https://www.udemy.com/course/sv-pre-uvm/
5

In reply to ben@SystemVerilog.us:

Hi
This code looks like after State went to Gate, then check TransCnt after some 0-10 clk cycles,
Actually i need to check the past values of TransCnt should be zero within 10 clk cycles.(Kind of reverse Check)

sequence s; ##[0:10] TransCnt; endsequence
property clkgate_state_p(bit reset);
  @(negedge TBCLK) disable iff(!reset) 
  (State_ps == 2)  |-> s.triggered;  
endproperty
6

In reply to naaj_ila:

You correct, I misapplied the use of endpoint.
In the past I used with the reapeat, like a[*10]


sequence s; a ##[1:2] 1; endsequence
b |-> a;

attempt       1   2   3   4   5   6   7   8
a             0   1   0   1   0   0   1   9
s.triggered           1   1               1    1 // 2nd and 7th attempt
s.triggered                   1   1              // 4th attempt
b                     1           1




sequence s; TransCnt ##[0:10] 1; endsequence
property clkgate_state_p(bit reset);
  @(negedge TBCLK) disable iff(!reset) 
  (State_ps == 2)  |-> s.triggered;  
endproperty

Apologies. Thanks for pointing this out.
Ben

7

In reply to ben@SystemVerilog.us:

Thanks a lot ben, It worked.
Actually there is big combination of code , i asked a small example.
I implemented in my code and it worked.

I understood very clearly how it is working.