In reply to dvuvmsv:
The Assertions are correct, but you have to understand what they mean and make the necessary
adjustments to do what you really need to specify.
ap_a2b: assert property( @(posedge clk) a |-> ##[2:5] b);
// Above states that at every attempt (the posedge clk) if(a) then within 2 to 5 cycles b==1.
//--------------------
ap_3athenb: assert property(@(posedge clk) a[*1:3] |-> b);
// at every attempt, all 3 threads of the Antecedent and consequent must be true for he Assertion to be true. Thus, for a true you need
a |->b and a[*2] |->b and a[*3] |-> b;
If a==0, that is a vacuous true.
Maybe what you need is just a[*3] |-> b
Or, maybe what you need is
First_match(a[*1:3]) |-> b
Remember, every attempt is separate from other attempts.
------------------------
ap_no3q_ab: assert property(@(posedge clk) not(a[*3] ##1 a[->1] intersect b[->1]));
// Thus says I should never see the sequence of 3 consecutive a
// that is followed at any time later by another a
// in the same time frame of no b's than a b.
//Thus, the following is an error condition because you have 4 a's in 1 1b
// a 1 1 1 0 0 0 0 0 1
// b 0 0 0 0 0 0 0 0 1
// Not a, aa, or aaa then another a and a&&b