I have an FSM which waits for state ABS which waits for signal ACK. once ACK is asserted it moves to next state BBS or in case it ACK is not asserted it waits for 100 clock cycles before moving to next stateBBS.
I want to write assertion to check that FSM is staying in the same state if ACK is not there before timeout.
and assertion for ,It moves to next state once either ACK is present or if ACK is not present, it should move to next state after timeout.
If we force state or ACK to different values it should give assertion failure.
/* The requirements are not clear. After rereading a few times, I think thta this is what you mean:
You have these objects:
typedef enum {ABS, BBS, XYZ} st_e;
st_e state;
bit clk, ack;
1) Upon a rose of state into ABS, state remains in that state until one of 2 conditions occur:
a) ack == 1
b) a timeout of 100 clock cycles
If condition "a" or "b" occurs, state transitions to BBS
*/
module m;
typedef enum {ABS, BBS, XYZ} st_e;
st_e state;
bit clk, ack;
// Conditions for state to go into BBS with the ack
ap_ABS2BBS: assert property(@ (posedge clk)
first_match($rose(state==ABS) ##1 state==ABS[*1:99] ##0 ack) |-> state==BBS);
// Conditions for state to go into BBS without the ack
ap_ABS_till_BBS: assert property(@ (posedge clk)
$rose(state==ABS) |-> ##1 state==ABS[*1:99] ##0 state==BBS);
endmodule
Yes you got the requirments correct.just one addition ACK should come before timeout or even present before the state ABS
But I wanted two write 2 assertions.
1.FSM is stays in the same state if ACK is not there before timeout.
2.FSM moves to next state once either ACK is present or if ACK is not present, it should move to next state after timeout.(is it possible to write in same assertion)
In reply to ben@SystemVerilog.us:
Yes you got the requirments correct.just one addition ACK should come before timeout or even present before the state ABS
But I wanted two write 2 assertions.
1.FSM is stays in the same state if ACK is not there before timeout.
// This does cover "the same state if ACK is not there before timeout"
// Conditions for state to go into BBS without the ack
ap_ABS_till_BBS: assert property(@ (posedge clk)
$rose(state==ABS) |-> ##1 state==ABS[*1:99] ##0 state==BBS);
2.FSM moves to next state onc_e either ACK is present or if ACK is not present, it should move to next state after timeout.(is it possible to write in same assertion)
// Previous assertion addresses "FSM moves to next state onc_e either ACK is present"
// Conditions for state to go into BBS with the ack
ap_ABS2BBS: assert property(@ (posedge clk)
first_match($rose(state==ABS) ##1 state==ABS[*1:99] ##0 ack) |-> state==BBS);
It is best to write multiple small assertions rather than one big one. If you insist on one big one, then convert the above two assertions into two separate properties (e.g., P1, P2) then write an assertion with (P1 or P2). There, you got one assertion with 2 ORed properties.
Harder to debug though!
:)
// Conditions for state to go into BBS without the ack
ap_ABS_till_BBS: assert property(@ (posedge clk)
$rose(state==ABS) |-> ##1 state==ABS[*1:99] ##0 state==BBS);
fails if ack is present .
FSM should move to next state if ACK is not present in this case , But only after 100 clk cycles. This assertion allows it to check before timeout
Errata : should be two separate properties (e.g., P1, P2) then write an assertion with (P1 and P2). There, you got one assertion with 2 ANDed properties.
$rose(state==ABS) |->
##1 state==ABS[*1:99] ##0 state==BBS);
// says if New ABS then starting from the next clock
// state==ABS is repeat 1 up to 99 more cycles
// until state==BBS
// a[*1:2] ##0 b is same as
// (a ##0 b) or (a ##1 a ##0 b)
// No, it does not fails if ack is present .
// ack is not even in this assertion.
// FSM should move to next state if ACK is not present in this case ,
// It does.
// NO on "But only after 100 clk cycles."
// This assertion allows it to check before timeout
// you need to understand the meaning of
// a[*1:2] ##0 b, see above; there is an "or"
IF we and p1 and p2 if ACK is not present throughout the timeout p2(ap_ABS2BBS) will fail and assertion will be error even if the p2 is fine.
Can you show example how to OR two properties .
Those 2 assertions have each a property; i just put the property content within the assertion statement.
Thus, declare the properties with property declaration.
Then write assert properly (P1 and P2) ;
It’s a AND because both properties must be true.
I believe that for a nonvacuity pass one of the 2 must be nonvacuous.
In general I prefer to have multiple smaller assertions, so I would not do this ANDing.
Do simulate the model.
In reply to Timus:
Those 2 assertions have each a property; i just put the property content within the assertion statement.
Thus, declare the properties with property declaration.
Then write assert properly (P1 and P2) ;
It’s a AND because both properties must be true.
I believe that for a nonvacuity pass one of the 2 must be nonvacuous.
In general I prefer to have multiple smaller assertions, so I would not do this ANDing.
Do simulate the model.
After Anding P1 and P2 in assertion.
its showing Success all overr simularion time and same with the OR
In reply to Timus:
1800 says: An evaluation attempt of a property of the form property_expr1 and property_expr2 is nonvacuous if, and only if, either the underlying evaluation attempt of property_expr1 is nonvacuous or the underlying evaluation attempt of property_expr2 is nonvacuous.
Thus, P1 and P2 is nonvacuous if either P1 or P2 is nonvacuous.
The assertions address all the requirements for the RTL model.
For the model to be correct it is necessary that ALL properties described
in the checking unit are correct. Each property describes a different
aspect of the requirements, thus you cannot say that under all test conditions
it is OK if one of them fails (you get that with the P1 or P2.
first_match($rose(state==ABS) ##1 state==ABS[*1:99] ##0 ack) |-> state==BBS);
// if the antecedent is a match then
// in the SAME cycle as ack state mus tb ==BBS
// If it does not, then it fails.
// The other property can still pass.
// BTW, you may want
first_match($rose(state==ABS) ##1 state==ABS[*1:99] ##0 ack) |-> ##1 state==BBS);