I am trying assertion for my following scenario but my logics not working trying to figure out what I missed in my logic
I want When entry is true, sig should be 0, for the entire duration of the next rising edge of rst.
I tried these logics but not working
property p_1;
@(posedge clk) disable iff (!rst)
entry |-> (sig == 0) throughout (rst[->1]);
endproperty
property p_2;
@(posedge clk) disable iff (!rst)
entry |-> (sig == 0) throughout ($rose(rst)[->1]);
endproperty
property p_3;
@(posedge clk) disable iff (!rst)
$rose(entry) |-> (sig == 0) throughout (rst[->1]);
endproperty
Remove disable iff condition.
check if following works :
property p_4;
@(posedge clk)
$rose(entry) |-> (sig == 0) until ($rose(rst));
endproperty
Can you please help me to understand why to remove disable iff we use until in your logic?
I tried these logics but not working
Could you please elaborate why the above 3 are not working as per expectation ?
Do you expect entry should be true as well as sig should be 0 for the entire duration when rst is false?
Yes, Entry should be high rst is high/toggle(goes High → low → High) in between and my sig value should be 0 at that time.
I didn’t quite get your intention. What is the requirement for rst ?
rst is high/toggle(goes High → low → High)
Do you even require to check rst ?
based on rst only I need to qualify
Could you please provide a running code example, maybe on EDAPlayground.com?
Developing properties works only on specific code. Anything else is guessing.