SVA: Local variable flow across "implies"

SystemVerilog
, , ,
1

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

2

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.

3

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