You need to read 1800’12 16.10 Local variables
d) 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:
…
I explain this in my book. Basically, 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. So what does that mean?
[code] property p1_ok;
bit v;
@(posedge clk) (a ##1 b, v=1) and @(posedge clk) v |=> d; // line 13
endproperty
assert property(p1_ok);
** Error: qst2.sv(13): Local variable v referenced in expression where it does not flow.
** Error: qst2.sv(15): The sva directive is not sensitive to a clock. Unclocked directives are not supported.
// Though there one local variable declaration called “v”, in reality, because of there are 2 threads separated by the AND operator, there exits 2 separate local variables, one v_for_thread1, and one v_for_thread2.
Will get back to you for more comments, but that is the issue.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115