Assertion stable after two or more rising edge

In reply to aming:

I tried with the first (the one with “first_match”) and now the assertion works fine, but at the end of simulation it remains append because (I guess) no more $fell(a) condition (second of the first part of the assertion) has been found.

If you want just one thread to start, and avoid this problem, you can exclude all others with something like the following


module m; 
  bit clk, a, b, dist_value; 
  bit start=1'b1; 
  always @(posedge clk) 
   if(!reset_n) start=1'b1; 
 
 function void reset_start(); 
    start=1'b0;
 endfunction 
 ap_q: assert property (@(posedge clk) disable iff (!reset_n) 
    first_match( ($fell(a) && start, reset_start()) ##[1:$] $fell(a)) |-> $stable(dist_value));

//Does this one work? $
fell(a) |=> $stable(b) until_with $fell(a); // until_with
// That assertion has a different meaning, stating that after the fell(a) you gt at next cycle stable(b). 
The original requirement stated that after the 2nd fell(a) you get the stable. 

Ben SystemVerilog.us