Assigning local variable within 'or' V/S 'and' operator

SystemVerilog
,
1

I was trying following code:

sequence s1;
    int x;
    ( (a ##1 b, x = data) or ( d ##1 e ) ) ##1 (data1 == x + 1); // local variable 'x' assigned in only 1 sequence
  endsequence  
 ap1:assert property( @(posedge clk) s1);

I observe following compilation:: Error: Local variable x referenced in expression where it does not flow.

Logically the error makes sense. Eg: when sequence ( d ## 1 e ) is true , ‘x’ is essentially uninitialized.

One of the solution is to assign local variable in both sequences of the ‘or’ operator.

sequence s2;
    int x;
    ( (a ##1b, x = data) or ( d ##1e, x = data) ) ##1 (data1 == x + 1);
  endsequence  
 ap2:assert property( @(posedge clk) s2);

However, when I use ‘and’ operator the following is legal:

sequence s3;
    int x;
    ( (a ##1 b, x = data) and (d ##1 e) ) ##1 (data1 == x + 1); // local variable 'x' assigned in only 1 sequence
  endsequence  
 ap3:assert property( @(posedge clk) s3);

and the following is illegal:

 sequence s4;
    int x;
    ( (a ##1 b, x = data) and (d ##1 e, x = data) ) ##1 (data1 == x + 1); // local variable 'x' assigned in both sequence
  endsequence
  ap4:assert property( @(posedge clk) s4);

**** Error: Local variable x referenced in expression where it does not flow.**

I am not clear on the following

  • Why is sequence s4 considered illegal ? What could the logical reason behind it be ?
  • Why is sequence s3 considered legal ( unlike sequence s1 ) ? When sequence ( d ## 1 e ) is true , won’t ‘x’ be unassigned ?

EDIT: The error with s1 exists only when local variable ‘x’ is used once after 'or’ed sequence

sequence s1;
    int x;
    ( (a ##1 b, x = data) or ( d ##1 e ) ) ##1 1; // No error although 'x' is assigned in only 1 sequence
  endsequence
2

In reply to Have_A_Doubt:
Consider this other example:




  sequence s4;
    int x;
    ( ((1, x = data) ##3 data==x) // seq1
    and 
    ( ##1 (1, x = data) ##1 data==x) ) // seq2
      ##1 data==x; //  seq3
  endsequence
  ap4:assert property( @(posedge clk) s4); 
  
  t0  x=data_@t0  // from seq1  
  t1  x=data_@t1  // from seq2
  t2  evaluate data==x // from seq2
   Question: which x to use? the x from x=data_@t0  or the x from x=data_@t1
  t3  evaluate data==x  // from seq1
  Question: which x to use? the x from x=data_@t0  or the x from x=data_@t1
  t4  evaluate data==x //  from seq3
  Question: which x to use? the x from x=data_@t0  or the x from x=data_@t1

  Please answer the question as to which do you want and why?  
You can argue the last but you can also argue for the variable contained (or braced) within each respective sequence. When you come out of the AND, then what? Which one to choose? 
That is the delemma! 
  Note that the sequences seq1,seq2 are both triggered concurrently and don't know of each other or their variables. The sequences are "braced" and don't communicate.

  That is the reason why an assignment to both concurrent threads (seq1, seq2) is illegal. 
 If a variable is assigned to only one of the threads, the local variable flows out; it's a rule defined in 1800

One can say: "well, take the last value assigned to the local variable as the value that flows out of the ANDed sequences. That does not work though. For example:


 sequence s4;
    int x;
    ( (a ##1b, x = data) and (d ##1e, x = data+2) ) ##1 (data1 == x); // local variable 'x' assigned in both sequence
  endsequence
  ap4:assert property( @(posedge clk) s4);  
Which x flows out? they are both assigned one cycle after the attempt.

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

3

In reply to ben@SystemVerilog.us:
Thanks Ben for the detailed explanation.

One more point I would like to add is that unlike ‘or’ operator , the ‘and’ operator requires that both LHS and RHS sequence match.
So unlike ‘or’ operator in sequence s1,using ‘and’ operator we wouldn’t have uninitialized local_variable ‘x’

4

In reply to ben@SystemVerilog.us:

Ben,
I was trying a few variations in the code.
I notice that following code is legal: edaplayground

whereas if I add a parenthesis around the ‘and’ operator, the sequence s1 is illegal ( for reasons pointed by you above )


sequence s1 ;  // Gives compilation error
    int x ; 
    (    
      ( a ##1 b, x = data , $display(" For 1, x == %0d ",x ) ) 
                   and
      ( d ##1 e, x = data , $display(" For 2, x == %0d ",x ) ) 
    )    //  Added parenthesis around the 'and' operator
           ##1  ( data1 == ( x + 1 ) ) ;
  ensequence

I am trying to understand without the parenthesis around the ‘and’ operator, how is the sequence ‘s1’ interpreted ? i.e Why is it legal that way ?

5

In reply to Have_A_Doubt:
Precedence will get you every time!
See 1800, page 390 Table 16-1—Operator precedence and associativity
See the precedence table (with examples) from my book.
I copied that table at https://photos.app.goo.gl/1WxWpo3HHi3TK68v5


// This
  sequence s1 ;
    int x ; 
// (    
    ( a ##1 b, x = data , $display("T:%0t For 1, x == %0d ",$time,x ) ) 
                   and
    ( d ##1 e, x = data , $display("T:%0t For 2, x == %0d ",$time,x ) )
//  )     //  Added parenthesis around the 'and' operator
           ##1  ( data1 == ( x + 1 ) ) ;
  endsequence
// is equivalent to 
  sequence s1 ;
    int x ; 
// (    
    ( a ##1 b, x = data , $display("T:%0t For 1, x == %0d ",$time,x ) ) 
                   and
    (( d ##1 e, x = data , $display("T:%0t For 2, x == %0d ",$time,x ) )
//  )     //  Added parenthesis around the 'and' operator
           ##1  ( data1 == ( x + 1 ) )) ;
  endsequence
//
// A simpler example from my book (link to table shown above) 
@c1 a ##1 @c2 b and c ##1 d 
// is equivalent to  
@c1 (a ##1 
       @c2 (b and c ##1 d))  
// is NOT equivalent to the following   
(@c1 a ##1 @c2  b) and (c ##1 d) // DOED NOT FOLLOW THE PRECEDENCE RULES
6

In reply to ben@SystemVerilog.us:

Ben,
So in the following case


sequence s1;
    int x;
 ( a ##1 b, x = data , $display("T:%0t For 1, x == %0d ",$time,x ) ) // seq1
    and 
 ( ( d ##1 e, x = data , $display("T:%0t For 2, x == %0d ",$time,x ) ) ##1 (data1 == (x + 1) )  );  //  seq2
       
  endsequence
  ap4:assert property( @(posedge clk) s1);

There is no error ( although local variable ‘x’ is assigned in both LHS (seq1) and RHS (seq2) sequence of ‘and’ operator ) as there is no discrepancy
for which value of ‘x’ is being used in expression: data1 == ( x + 1 ) i.e the value of ‘x’ assigned in seq2 is being used expression

7

In reply to Have_A_Doubt:
It behaves as 2 separate variables, one for each sequence. Thus, it is equivalent to:


sequence s1;
    int x1, x2;
 ( a ##1 b, x1 = data , $display("T:%0t For 1, x1 == %0d ",$time,x ) ) // seq1
    and 
 ( ( d ##1 e, x2 = data , $display("T:%0t For 2, x == %0d ",$time,x ) ) ##1 (data1 == (x2 + 1) )  );  //  seq2
 
  endsequence
  ap4:assert property( @(posedge clk) s1);
8

In reply to ben@SystemVerilog.us:

For the following sequence


sequence s1;
    int x;
 ( a ##1 b, x = data , $display("T:%0t For 1, x == %0d ",$time,x ) ) // seq1
    and 
 ( ( d ##1 e, x = data , $display("T:%0t For 2, x == %0d ",$time,x ) ) ##1 (data1 == (x + 1) )  );  //  seq2
  endsequence

Scope of local variable ‘x’ is within sequence s1.This means seq1,seq2 both have access to it.

It behaves as 2 separate variables, one for each sequence.

So seq1 isn’t aware whether seq2 assigns to it as well. Essentially behaving as 2 separate variables

9

In reply to Have_A_Doubt:

So seq1 isn’t aware whether seq2 assigns to it as well. Essentially behaving as 2 separate variables

YES. You see that clearly on tools that use thread viewers that display each thread and the variables associated with them.
Logically, that makes sense. What if in the same cycle x=data1 in the LHS of the AND sequence, and it assigns x=data2 on the RHS of the AND sequence. What is the value of x? you can’t define it if x is a common single variable.

10

In reply to ben@SystemVerilog.us:

Ben,
Have 2 further questions:
1)

sequence s4;
int x;
( ((1, x = data) ##3 data==x) // seq1
and
( ##1 (1, x = data) ##1 data==x) ) // seq2
##1 data==x; // seq3
endsequence
ap4:assert property( @(posedge clk) s4);
t0 x=data_@t0 // from seq1
t1 x=data_@t1 // from seq2
t2 evaluate data==x // from seq2
Question1: which x to use? the x from x=data_@t0 or the x from x=data_@t1
t3 evaluate data==x // from seq1
Question2: which x to use? the x from x=data_@t0 or the x from x=data_@t1
t4 evaluate data==x // from seq3
Question3: which x to use? the x from x=data_@t0 or the x from x=data_@t1
Please answer the question as to which do you want and why?

Doesn’t the discrepancy lie with only question3 ?
For Q1: Shouldn’t the ‘x’ from seq1 be used ?
For Q2: Shouldn’t the ‘x’ from seq2 be used ?
For Q3: Should ‘x’ from seq1 or seq2 be used ? Not clear hence the compilation error

  1. Consider the following ‘or’ operator :

   sequence s2;
    int x;
    ( (a ##1 b, x = data1) or ( d ##1 e, x = data2) ) ##1 (data == x + 1);
  endsequence  
  ap2:assert property( @(posedge clk) s2);

Although the code is legal, doesn’t there exist a discrepancy with which value of ‘x’ is used while evaluating expression : (data == x + 1) ?

Assuming both sequences are true for ‘or’, ‘x’ would be assigned possibly different values at the same time.

11

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

12

In reply to ben@SystemVerilog.us:

Thanks Ben.

So to answer my questions from previous reply:
1)

Doesn’t the discrepancy lie with only question3 ?
For Q1: The ‘x’ assigned from seq1 would be used.
For Q2: The ‘x’ assigned from seq2 would be used
For Q3: Should ‘x’ from seq1 or seq2 be used ? Not clear hence the compilation error

There exists discrepancy with question3, hence the compilation error: Local variable x referenced in expression where it does not flow.

Although the code is legal, doesn’t there exist a discrepancy with which value of ‘x’ is used while evaluating expression : (data == x + 1) ?

The equivalent expression is:


  ( (a ##1 b, x=data1) ##1 (data == x + 1)) or ( ( d ##1 e,x=data2) ##1 (data == x + 1) ) ;

So there is no discrepancy , the expression ( data==x+1) would use the value of ‘x’ assigned in respective sequence.