I changed the model and provided explanations in the comments.
EDA EDA Playground
module tb;
bit clk, a, b;
initial forever #5 clk = !clk;
default
clocking def_clk @(posedge clk);
endclocking
function void print(string msg);
$display("T : %0t %s", $time(), msg);
endfunction
int cnt2, cnt3 ;
function void dbg(int v, id);
$display("id %d, v_cnt : = %0d", id, v);
if(id==2) cnt2 = v;
if(id==3) cnt3= v;
endfunction
//property p_pulse_cnt(N); // Doesn't work
// int v_cnt;
// // ($rose(a), v_cnt=0) ##1 first_match( ($fell(b), v_cnt++, dbg(v_cnt))[=1:$] ##1 $fell(a) ) |=> ( v_cnt == N, dbg(v_cnt) ) ;
// ($rose(a), v_cnt=0) ##1 ( ( ($fell(b), v_cnt++, dbg(v_cnt))[=1:$] ) intersect !a[->1] ) |=> ( v_cnt == N, dbg(v_cnt) ) ;
//endproperty
property p_pulse_cnt_2(N);
int v_cnt;
// ($rose(a), v_cnt=0) ##1 ( ( ($fell(b)[->1], v_cnt++, dbg(v_cnt, 2))[+] ##[1:$] !a ) intersect !a[->1] ) |=> ( v_cnt == N, dbg(v_cnt) ) ;
($rose(a), v_cnt=0) ##1 ( ( ($fell(b)[->1], v_cnt++, dbg(v_cnt, 2))[+] ) intersect !a[->1] ) |=> ( v_cnt == N); // , dbg(v_cnt) ) ;
endproperty
/* $rose(a), v_cnt=0) ##1 ( ( ($fell(b)[->1], v_cnt++, dbg(v_cnt, 2))[+] ) intersect !a[->1] ) is of the form
A ##1 (B[->1][*1:$] intersect C[->1]) // same as
A ##1 (!B[*0:$] ##1 B[*1] intersect C[->1]) or // thread 1 carries its separate v_cnt
.. if thread 1 is shorter thatn the length of c[->1] then this thread is a NO MATCH
A ##1 (!B[*0:$] ##1 B[*4] intersect C[->1]) or
---if C occurs in thread 4 before the occurrence of B, then this thread is a NO MATCH
--- All future threads are also NO MATCH since c[->1 already occurred ]
---These future threads are: A ##1 (!B[*0:$] ##1 B[*1] intersect C[->1])
--- With a NO MATCH in any of the antecedents, the assertion is vacuously true.
*/
property p_pulse_cnt_3(N);
int v_cnt;
// ($rose(a), v_cnt=0) ##1 ( ($fell(b)[->1], v_cnt++, dbg(v_cnt, 3))[+] within !a[->1] ) |=> ( v_cnt == N, dbg(v_cnt) ) ;
($rose(a), v_cnt=0) ##1 ( ($fell(b)[->1], v_cnt++, dbg(v_cnt, 3))[+] within !a[->1] ) |=> ( v_cnt == N); // , dbg(v_cnt) ) ;
endproperty
/* 1800: The construct seq1 within seq2 is an abbreviation for the following:
(1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2*/
// Thus, $fell(b)[->1][*1:$] within !a[->1] // is equivalent to
/* (1[*0:$] ##1 $fell(b)[->1][[*1:$] ##1 1[*0:$]) intersect !a[->1] // equivalent to:
(1[*0:$] ##1 $fell(b)[*1] ##1 1[*0:$]) intersect !a[->1] or // thread 1 carries its separate v_cnt
(1[*0:$] ##1 $fell(b)[*2:$] ##1 1[*0:$]) intersect !a[->1] // threads 2 to $, each carrying their own v_cnt
FOr thia assertion to succeed, all antecedents must succeed
Also, eah thread of the antecedent carries its own local variable.
When thread 1 of the antecedent is a match, the consequent ( v_cnt == N) is a no match (v_cnt==1, N==3)
Thus, assertion fails.
*/
//assert property( p_pulse_cnt (3) ) print("PASS ast_pulse_count"); //Doesn't work
ap_pulse_cnt_2: assert property( p_pulse_cnt_2(3) ) print("PASS ast_pulse_count");
ap_pulse_cnt_3: assert property( p_pulse_cnt_3(3) ) print("PASS ast_pulse_count");
//else print("FAIL ast_pulse_count");
// initial begin $dumpfile("dump.vcd"); $dumpvars(); end
initial begin
## 5 a = 1;
##10 a = 0;
##5;
$finish(2);
end
initial begin
## 5 b = 1;
## 1 b = 0;
## 1 b = 1;
## 1 b = 0;
## 3 b = 1;
## 2 b = 0;
end
endmodule
