In reply to Aryan_Jogur:
Question: Can the common local variable be assigned in one sequence and use that in another intersecting sequence?
Answer: NO
Elaboration on the use of local variable in AND / OR sequences
From my SVA 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.
A quick explanation is provided below
And for the Anding:
Consider this simple test:
bit clk, a, b, c=1'b1, d;
initial forever #10 clk = !clk;
property p_and;
bit v;
$rose(a) |-> ((b, v=c) ##3 v==c)and (c ##1 (1, v=d) ##2 v==c);
endproperty
ap_and: assert property(@(posedge clk) p_and);
property p_and_equivalent;
bit v1, v2;
$rose(a) |-> ((b, v1=c) ##3 v1==c)and (c ##1 (1, v2=d) ##2 v2==c);
endproperty
ap_and_equivalent: assert property(@(posedge clk) p_and_equivalent);
If the local variable “v” is used as the identical variable, then there are issues because both sequence threads of the and / intersect are concurrent.
There is a way to force the use of the same variable for both threads, but then you have to model it using the task techniques explained in my paper Understanding the SVA Engine,
Verification Horizons
Here is the model (complete model at http://SystemVerilog.us/vf/flow_and.sv )
// Desired Equivalent model (with common local variable)
// ((b, v=c) ##3 v==c)
task automatic t_b(ref bit v, done, err);
if(b) begin
v=c;
repeat(3) @(posedge clk) ;
assert(v==c) else err=1;
$display("%t t_b.v==%b", $realtime, v);
done=1'b1;
end
else err=1'b1;
done=1;
endtask
// (c ##1 (1, v=d) ##2 v==c)
task automatic t_c(ref bit v, done, err);
if(c) begin
@(posedge clk);
v=d;
repeat(2) @(posedge clk) ;
assert(v==c) else err=1'b1;
$display("%t t_c.v==%b", $realtime, v);
done=1'b1;
end
else err=1'b1;
done=1'b1;
endtask
task automatic t_and();
bit z, done1, done2, err;
fork
t_b(z, done1, err);
t_c(z, done2, err);
join_none
wait(done1 && done2);
assert(err==0);
endtask
always_ff @(posedge clk) begin
fork t_and(); join_none
end
In my book, I go over this other code example with some explanations in the comments.
Hope this helps. http://SystemVerilog.us/vf/or_multi2.sv
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
- SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
- Free books: Component Design by Example https://rb.gy/9tcbhl
Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
- Papers:
