In reply to a72:
For the developers to not execute it for efficiency reasons does not make sense. I wanted to know the final value of 'y' after one or more of the OR threads pass. If a thread is slated to execute, it must be executed.
If your interest is on the y, write a separate assertion with only the following as the consequent
(d ##2 e, y = data2, $display($stime,,,"From seqeunce D E complete y=%0b",y) ) ##1 (1'b1,$display($stime,,,"y=%b",y) );
Actually, optimization DOES
make sense. There is no requirement in 1800 to provide extra information as long as the assertion meets the 1800 requirements (pass or fail).
You do that as a person. For example, you want either a veggie burger with tomatoes on a wheat bun (ANDing) or
a salad that includes (the and)shrimp. The attendant says I have the salad and the shrimp, but I have no tomatoes and on the burger, I only have the kind ...
** You interrupt and say, "never mind on the burger; I have no interest if it's regular meat or veggie burger since you did not match my interest with tomatoes"
. Why did you short-circuit the conversation with the attendant? .. because you're hungry? time is of value?
A bit more on local variables. From my book:
2.7.9 Local variables in concurrent and, or, and intersect threads (rule 14)
Rule: When local variables are used in sequences that have concurrent threads, it is possible that the values of the local variables may not be assigned, or assigned by one thread and not the other, or assigned in both threads at the same or at different cycles with different values. Concurrent threads in sequences occur with the use of the and, or, and intersect operators.  In general, there is no guarantee that evaluation of the two threads results in consistent values for the local variable, or even that there is a consistent view of whether the local variable has been assigned a value. Therefore, the values assigned to the local variable before and during the evaluation of the composite sequence are not always allowed to be visible after the evaluation of the composite sequence. Below are some examples of local variable flow.
// ORing causes 2 separate threads, each with local copies of local variables (LV).
// In each thread, the LVs must have a value before being read.
sequence q_err; int x;
(a ##1 (b, x=dt) ##1 c) or
(d ##1 e==x); // x read, but not written
ap: assert property(@(posedge clk)q_no_out_flow);
bit v, v2;
((a, v=x) ##1 b) and // also for the intersect
(c ##1 (d, v=y))
##1 v==1; // v is blocked from flowing out // because it is common to both threads
endsequence : q_no_out_flow
// ** Error: Local variable v referenced in expression where it does not flow.