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