In reply to peter:
Updated model: (1) - EDA Playground
https://photos.app.goo.gl/meM2MwSrJESfSqF58
//
module m;
bit clk, vld, req, ack, rst_n=1;
int count=2, pass1, pass2, pass3, err1, err2, err3;
initial forever #10 clk = !clk;
property vld_tog_chk (req, ack, vld, count);
int v;
@(posedge clk) disable iff (!rst_n)
##1 ($rose(req), v=count) |-> //( //strong(
first_match((vld[->1], v=v-1, $display("%t (1) v=%d", $realtime, v))[*1:$] ##1 !vld[*0:$] ##1 ($rose(ack), $display("%t (2) v=%d", $realtime, v))) ##0 v>=0;
endproperty: vld_tog_chk
ap_vld_tog_chk: assert property(vld_tog_chk(req, ack, vld, count)) pass1=pass1+1; else err1=err1+1;
ap_vldack: assert property(@(posedge clk) disable iff (!rst_n)
##1 $rose(req) |-> ( //strong(
first_match(vld[=2] ##1 $rose(ack)) ##0 ack && !vld)) pass2=pass2+1; else err2=err2+1;
property vld_tog_chk2 (req, ack, vld);
@(posedge clk) disable iff (!rst_n)
##1 $rose(req) |-> //strong
// (vld[=2] ##[1:$] $rose(ack));
(vld[=2] ##1 $rose(ack));
endproperty: vld_tog_chk2
ap_vld_tog_chk2: assert property( vld_tog_chk2(req, ack, vld)) pass3=pass3+1; else err3=err3+1;
initial begin :init1
$dumpfile("dump.vcd"); $dumpvars;
repeat (1) @(posedge clk);
req <= 1'b1;
repeat(2) begin :rpt1
@(posedge clk);
vld<= 1; req<=0; ack <=0;
@(posedge clk);
vld<= 0; req<=0;
repeat(2) @(posedge clk);
end :rpt1
ack <=1;
@(posedge clk) req<=1; ack<=0;
repeat(3) begin
@(posedge clk);
vld<= 1; req<=0; ack <=0;
@(posedge clk);
vld<= 0; req<=0;
repeat(2) @(posedge clk);
end
ack <=1;
repeat(2) @(posedge clk);
$finish;
end
endmodule
50 (1) v= 1
130 (1) v= 0
190 (2) v= 0
230 (1) v= 1
310 (1) v= 0
390 (1) v= -1
"testbench.sv", 15: m.ap_vldack: started at 190ns failed at 390ns
Offending '$rose(ack)'
"testbench.sv", 25: m.ap_vld_tog_chk2: started at 190ns failed at 390ns
Offending '$rose(ack)'
450 (2) v= -1
$finish
Now compare above with (2) - EDA Playground
property vld_tog_chk2 (req, ack, vld);
@(posedge clk) disable iff (!rst_n)
##1 $rose(req) |-> //strong
(vld[=2] ##[1:$] $rose(ack)); // <---------
//(vld[=2] ##1 $rose(ack));
endproperty: vld_tog_chk2
ap_vld_tog_chk2: assert property( vld_tog_chk2(req, ack, vld)) pass3=pass3+1; else err3=err3+1;
(vld[=2] ##[1:$] rose(ack)); // is same as
!vld[*0:] ##1 vld ##1 !vld[*0:] ##1 vld ##1 !vld[*0:] ##[1:$] rose(ack)
I am puzzled on (vld[=2] ##[1:] $rose(ack)) because it should fail with 3 vld before ack.
I’ll work on this with my full version of the simulator (rather than the eda version).
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
- 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
- A Pragmatic Approach to VMM Adoption
http://SystemVerilog.us/vf/VMM/VMM_pdf_release070506.zip
http://SystemVerilog.us/vf/VMM/VMM_code_release_071806.tar
- Papers and publications
SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy
Reflections on Users’ Experiences with SVA, part 1
Reflections on Users’ Experiences with SVA | Verification Horizons - March 2022 | Verification Academy
Reflections on Users’ Experiences with SVA, part 2
Reflections on Users’ Experiences with SVA, Part II | Verification Horizons - July 2022 | Verification Academy
Understanding and Using Immediate Assertions
Understanding and Using Immediate Assertions | Verification Horizons - December 2022 | Verification Academy
SUPPORT LOGIC AND THE ALWAYS PROPERTY
http://systemverilog.us/vf/support_logic_always.pdf
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
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/