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