Does a local variable flow across the “implies” operator?
Consider the two properties below.
property prop1;
logic [7:0] curr_val;
(en_d, curr_val = inval1_d) |-> ((curr_val + 4’d4) == out1);
endproperty
property prop2;
logic [7:0] curr_val;
(en_d, curr_val = inval1_d) implies ((curr_val + 4’d4) == out1);
endproperty
Are these equivalent in terms of local variable flow?
Should the second one result in an error?
I’ve seen some online discussions of something like this from the time of the LRM development.
https://www.eda-twiki.org/sv-ac/hm/9413.html
How was this discussion resolved?
Thanks
The proposal got dropped. 03195: Local Variables Flow Out Issue in and/or/intersect/implies - Accellera Mantis
It’s not an error, but each thread of an assertion gets its own copy of the local variable. Using implies
creates threads for both the antecedent and consequent.
Dave, Thank you for your explanation. One more follow-up.
As each thread gets its own copy, is there a way to tie them together.
For example, something like the equality in the antecedant. Or is that something that has no effect on the copy of the variable in the consequent?
property prop2;
logic [7:0] curr_val;
(en_d && (curr_val == inval1_d), curr_val = inval1_d) implies ((curr_val + 4’d4) == out1);
endproperty