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
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.
// $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
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)