This is a follow-up model to the question
https://verificationacademy.com/forums/systemverilog/can-common-local-variable-be-assigned-one-sequence-and-use-another-intersecting-sequence
In the above link, I explain the SVA rules of local variables when using concurrent sequences with the and, or, intersect. In this post, I am showing 4 models
- SVA Model
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);
- Equivalent SVA model in SVA
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);
- Desired task model to force the use of the same local variable in both sequences
- Equivalent SVA model using tasks
The concept of the task models is explained in my paper Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy
The simulation model is below and at at http://SystemVerilog.us/vf/flow_and.sv
The simulation statistics are at http://SystemVerilog.us/vf/sim_stats.png
Key elements of these task models is the use of fork - join_none tasks and arguments passed by reference. I agree that it is hard to follow, and this is why SVA is nice in that it is rather compact.
However, understanding the model helps in writing better SVA code, my belief because you get a better understanding of the equivalent inner works. Note that the actual implementation by vendors is different; what I am showing is an equivalency. The model:
module top;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, a, b;
bit c, d;
int err_count_task, err_count_sva;
event e_tand, e_sva;
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);
//***********************DESIRED NON-SVA AND NON-EQUIVALENT MODEL
// where local variables are visible in concurrent sequences
// (SVA handles this as separate copies for each sequence)
// $rose(a) |-> ((b, v=c) ##3 v==c)and (c ##1 (1, v=d) ##2 v==c);
// 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 err=%b", $realtime, v, err);
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;
bit done1, done2, err1, err2;
if($rose(a, @(posedge clk) )) begin : antc // antecedent match
fork
t_b(z, done1, err1);
t_c(z, done2, err2);
join_none
wait(done1 && done2);
p_nonSVA_Model: assert(err1==0 && err2==0) else begin
-> e_tand;
err_count_task+=1'b1;
end
end : antc
endtask
// ********************** TASK MODEL PER SVA RULES
// $rose(a) |-> ((b, v=c) ##3 v==c)and (c ##1 (1, v=d) ##2 v==c);
task automatic t_sva();
bit z1, z2;
bit done1, done2, err1, err2; //z1, z2 local variables of the property
if($rose(a, @(posedge clk) )) begin // antecedent match
fork
t_b(z1, done1, err1); // Note the separate local variables passed to
t_c(z2, done2, err2); // each thread
join_none
wait(done1 && done2);
p_model_sva: assert(err1==0 && err2==0) else begin
-> e_sva;
err_count_sva +=1'b1;
end
end
endtask
always_ff @(posedge clk) begin
fork
t_and();
t_sva();
join_none
end
initial begin
repeat (300) begin
@(posedge clk);
if (!randomize(a, b, c, d) with {
a dist {1'b1 := 1, 1'b0 := 1};
b dist {1'b1 := 1, 1'b0 := 0};
d dist {1'b1 := 1, 1'b0 := 4};
})
`uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule
========================================================
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 | Verification Academy
- Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb - Papers:
- Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy - SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy - SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy