In reply to Have_A_Doubt:
Here are the rules, as described in my book. I suggest that you run some simulations and verify those concepts.
2.7.9.2 Variables assigned on parallel “and” “intersect” threads
Rule: [1800] In the case of and and intersect, a local variable that flows out of at least one operand shall flow out of the composite sequence unless it is blocked. A local variable is blocked from flowing out of the composite sequence if either of the following statements applies: 1) The local variable is assigned in and flows out of each operand of the composite sequence, or 2) The local variable is blocked from flowing out of at least one of the operand sequences. The value of a local variable that flows out of the composite sequence is the latest assigned value. The threads for the two operands are merged into one at completion of evaluation of the composite sequence.
When two sequences are ANDed or INTERSECTed, each sequence produces its own thread. However, unlike the ORing of two sequences, the and/intersect of two sequences produces a single end point at the termination of the threads. This means that the two threads merge into a single starting point; this contrasts to the Oring of two sequences where each thread is carried separately to the next sequence. If the sequence makes assignments to local variables, then each of the sequence involved in the ANDing or INTERSECTing carries its own individual and separate copy of the local variables. However, only those local variables that are NOT assigned in both threads flow out of the sequence. This concept is shown graphically in Figure 2.7.9.2. Thus, it is illegal to have the same variables being assigned in each of the threads and have that variable flow out of the sequence because the outputs of these operators produce a single end point with updated values for the variables.
2.7.9.1 Variables assigned on parallel “or” threads
Rule: When two sequences are ORed, each sequence produces its own thread that can get carried through to the next step, such as an end point (no more continuity), concatenation with another sequence, or as antecedent to a consequent. For example,
(sequence1 or sequence2) ##1 seq3 // is equivalent to (sequence1 ##1 sequence3) or (sequence1 ## sequence3) // two threads
Note that multithreaded sequence do occur with range operators.
If the sequence makes assignments to local variables, then each of the sequence involved in the ORing carries its own individual and separate copy of the local variables. Those separate copies of the local variables are carried all the way through each of the ORed sequence thread. This concept is shown graphically in Figure 2.7.9.1.
…
//Consider the following property:
property p_abv;
bit v;
(a, v=1) or (b, v=0) |=> v==1; // (all threads of antecedent must be tested with the ORing
endproperty
// The equivalent property to p_abv is the following:
property p_abv_eqv;
bit v1, v2;
( (a, v1=1'b1) |=> v1==1) and
( (b, v2=1'b0) |=> v2==1);
endproperty : p_abv_eqv
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog