In reply to ben@SystemVerilog.us:
The comments in the code below explain why
THUS: vld[=2] ##[1:$] rose(ack))) is equivalent to
vld[->2] ##[1:] $rose(ack))) */
// 2 vld between req ack
module m;
bit clk, vld, req, ack, rst_n=1;
int count=2, pass1, pass2, pass3,pass4, pass5, err1, err2, err3, err4, err5;
initial forever #10 clk = !clk;
// number of vld is dynamic
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)[*1:$] ##1 !vld[*1:$] ##0 $rose(ack)) ##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;
// Correctly using the Non-consecutive repetition, Boolean [=n]
ap_vldack_ok: assert property(@(posedge clk) disable iff (!rst_n)
##1 $rose(req) |-> ( //strong( says after 2 vld an ack
(vld[=2] ##1 $rose(ack)) ##0 !vld)) pass2=pass2+1; else err2=err2+1;
// Correctly using the goto, Boolean [->n]
ap_vldack_ok2: assert property(@(posedge clk) disable iff (!rst_n)
##1 $rose(req) |-> ( //strong( says after 2 vld an ack
first_match(vld[->2] ##1 !vld[*1:$] ##1 $rose(ack)) ##0 !vld)) pass3=pass3+1; else err3=err3+1;
// Incorrectly using the Non-consecutive repetition, Boolean [=n]
ap_vldack_bad: assert property(@(posedge clk) disable iff (!rst_n)
##1 $rose(req) |-> ( //strong(
vld[=2] ##[1:$] $rose(ack))) pass4=pass4+1; else err4=err4+1;
// Equivalencey to the Non-consecutive repetition, Boolean [=n]
ap_vldack_bad_equiv: assert property(@(posedge clk) disable iff (!rst_n)
##1 $rose(req) |-> ( //strong(
vld[->2] ##1 !vld[*0:$] ##[1:$] $rose(ack))) pass5=pass5+1; else err5=err5+1;
// consequent is equivalent to
/* vld[->2] ##1 !vld[*0] ##[1:$] $rose(ack) or // Thread1
vld[->2] ##1 !vld[*1] ##[1:$] $rose(ack) or ...
Considering thread1 only, the assertion will will be satisfied (a pass) with the sequence
... vld ... vld .. ... %rose(ack) // because
vld[->2] ##1 !vld[*0:$] ##[1:$] $rose(ack) // is same as
vld[->2] ##1 !vld[*0] ##1 $rose(ack) or // <<<---- ThIS THREAD
vld[->2] ##1 !vld[*0] ##2 $rose(ack) ##1 $rose(ack) or
..
// Consider just THIS THREAD
vld[->2] ##1 !vld[*0] ##1 $rose(ack) // it simplies to just
vld[->2] ##1 $rose(ack) // thus,
Two vld (the vld[->2]) folowed $rose(ack) satifies the consiquent
THUS: vld[=2] ##[1:$] $rose(ack))) is equivalent to
vld[->2] ##[1:$] $rose(ack))) */
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