In the following assertion what will be the value of x if both subsequences end at the same time? Will it be indeterministic?
sequence s1;
int x;
((a ##[1:5] b, x = data1) or (d ##2 e, x = data2)) ##1 (data == x);
endsequence
if both subsequences (a ##[1:5] b) and (d ##2 e) match at the same time, what will be the value assigned to x?
Thanks.
In reply to a72:
From my SVA book:
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
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.
// Consider the following property:
property p_abv;
bit v;
(a, v=1) or (b, v=0) |=> v==1;
endproperty : p_abv
/* The antecedent of this property has two threads (a, v=1) and (b, v=0); each of those thread carries its own individual copy of the local variable. In the consequent, each antecedent thread must be evaluated with consequent. In this case, the individual copy of the local variable for each thread is carried into the consequent when that thread is evaluated. Thus for thread (a, v=1) the v in the consequent is the copy used in that thread. Similarly, for thread (b, v=0) the v in the consequent is the copy used in that thread. 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
// In the above example, if a==1'b1, and b==1'b1, then the property will fail.
Your property:
sequence s1;
int x;
((a ##[1:5] b, x = data1) or (d ##2 e, x = data2)) ##1 (data == x);
endsequence
// Is same as:
sequence s1;
int x1, x2;
((a ##[1:5] b, x1 = data1) ##1 (data == x1)) or
((d ##2 e, x2 = data2) ##1 (data == x2));
endsequence
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
SUPPORT LOGIC AND THE ALWAYS PROPERTY
http://systemverilog.us/vf/support_logic_always.pdf
SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.
Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/
Thanks much, Ben. Have been using local variables for some time now, but wasn’t aware of these nuances.
I had created an example to see how this works. Here’s the EDA playground link.
The assertion is the same as posted above except that I added a few $display statements attached to sub-sequences.
sequence s1;
int y, y1;
( (a ##[1:5] b, y = data1, $display($stime,“From sequence s1 : A B complete y=%0b”,y)) ) or
(d ##2 e, y = data2, $display($stime,“From seqeunce D E complete y=%0b”,y) ) ##1 (1’b1,$display($stime,“y=%b”,y) );
endsequence
When I simulate this, the subsequence " ##1 (1’b1,$display($stime,“y=%b”, y) ); " never gets executed, even when one of the OR subsequence is satisfied. I don’t understand that. Please see the EDA playground example.
Thanks in advance.
In reply to a72:
Before responding to your specific question, let me take this simple assertion.
Should the assertion pass or fail?
property p1;
int v;
(1, v=0) ##[1:2] (1, v=v+1) ##0 v==2;
endproperty
ap1: assert property(@ (posedge clk) p1);
// It fails because it has 2 threads, and each thread has its own separate copy
// of the local variable. It is equivalent to
((1, v=0) ##[1] (1, v=v+1) ##0 v==2) or // This "v" is separate from
((1, v=0) ##[2] (1, v=v+1) ##0 v==2); // this "v"
// Note: v==1 at the end of each thread
// Each thread has its own local variable v
The thread viewer demonstrates this very well.
See below for your specific model.
http://systemverilog.us/vf/temp1016.sv
When I simulate this, the subsequence " ##1 (1’b1,$display($stime,“y=%b”, y) ); " never gets executed, even when one of the OR subsequence is satisfied. I don’t understand that.
In a consequent, you are looking for a PASS. Thus, if either thread of an ORing sequence matches, then there is NO NEED to test the other thread.
See the thread viewer below.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
Ben, Thanks very much. One step forward. I think I understand.
You mention:
In a consequent, you are looking for a PASS. Thus, if either thread of an ORing sequence matches, then there is NO NEED to test the other thread.
Agree.
Also, you have mentioned
((sequence1 or sequence2) ##1 seq3
// is equivalent to
(sequence1 ##1 sequence3) or (sequence1 ##1 sequence3)
I still have a question on my case, though. In my case, when sequence1 (namely, ( (a ##[1:5] b, y = data1, $display($stime,“From sequence s1 : A B complete y=%0b”,y)) ) passes, shouldn’t the " ##1 (1’b1,$display($stime,“y=%b”, y) ); " execute? I understand that the second thread of OR is a don’t care since first thread passes. But once the first thread passes, shouldn’t the " ##1 (1’b1,$display($stime,“y=%b”, y) ); " subsequence execute?
Hope the question makes sense. If not, please don’t bother.
Thanks.
In reply to a72:
TYpo in your equivalence. It should be
((sequence1 or sequence2) ##1 seq3
// is equivalent to
(sequence1 ##1 sequence3) or (sequence2 ##1 sequence3)
But once the first thread passes, shouldn’t the " ##1 (1’b1,$display($stime,“y=%b”, y) ); " subsequence execute?
The simulator can execute any concurrent threads in any order.
In this case, it completed the the attempted at time 15 and the next 2 threads at time 25.
At time 35 it started thread 1 and discovered that the sequence ended with a match, thus deducting that the assertion is a PASS. For efficiency reasons, it dropped any further calculations (i.e., the ##1 (1’b1,$display($stime,“y=%b”, y) ). Do you see any reasons as to why it should finish the second thread?
:)
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
I spent hours trying to figure out why " ##1 (1’b1,$display($stime,“y=%b”, y) )" was not being executed. 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.
But thanks very much for taking time to explain the concepts in such detail. I learnt a lot. Much appreciated. Thanks.
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. [1] 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);
sequence 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.