In reply to ben@SystemVerilog.us:
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
Ben, Please help me understand.
you mentioned
"
//--------------------
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;
"
so if a is only triggered once before b i.e a |-> b then the assertion ap_3athenb failed ? according LRM a[*1:3] is same as a OR a[*2] OR a[*3]. Does it mean any of a |-> b, a[*2] |->b, a[*3] |-> b in this assertion is true then assertion successes.
THanks