In reply to Have_A_Doubt:
Generally b[=m] means that ‘b’ must be true on ‘m’ clocks (not necessarily consecutive)
So b[=0] would mean that ‘b’ must be true on ‘0’ clocks i.e ‘b’ should never be true.
The same can be cross checked via it’s equivalent expression: !b[*0:$] i.e ‘b’ should never be true.
However the assertion passes/fails on the very 1st clock that the consequent is evaluated using
property ab;
@(posedge clk) a |=> b[=0];
endproperty
b[=1] is same as !b[*0:$] ##1 b[*1] ##1 !b[*0:$]
// There are many ORed threads.
b[=1] !b[*0:$] ##1 b[*1] ##1 !b[*0:$] // as a reference
// For the "=0"
b[=0] !b[*0:$] ##1 b[*0] ##1 !b[*0:$] // is same as
//
!b[*0] ##1 !b[*0] ##1 !b[*0] or
!b[*0] ##1 !b[*0] ##1 !b[*1] or
!b[*0] ##1 !b[*0] ##1 !b[*n]
// COnsider those threads and reducing them because a[*0] ##1 b is same as b
!b[*0] ##1 !b[*0] ##1 !b[*0] // is same as
!b[*0]
!b[*0] ##1 !b[*0] ##1 !b[*1]
!b[*1] // same as
Thus, you say that b[=0] is same as
!b[*0] or !b[*1] or !b[*2] or ...
// FOr your
a |=> b=0]; // same as
a |=> !b[*0] or !b[*1] or !b[*2] or ...
// Thus, b[=0] is NOT the same as always !b and
// the assertion passes/fails on the very 1st clock that the consequent is evaluated
// It would pass because of the !b[*1]
**
On the always**
always [cycle_delay_const_range_expression] property_expr Evaluates to true (vacuous or nonvacuous true) if property_expr holds at every current or future clock tick that is within the range of clock ticks specified by const_range. It is not required that all clock ticks within this range exist.
always [cycle_delay_const_range_expression] property_expr Evaluates to true (vacuous or nonvacuous true) if property_expr holds at every current or future clock tick that is within the range of clock ticks specified by const_range. It is not required that all clock ticks within this range exist.
@(posedge clk) a |=> s_always[1:10]!b
In the cycle after “a” (T0) then starting from the next cycle (T1) b== until T10.
The max range cannot use the $, but you can use a 2^31 (syntax? forgot it, sorry)
I don’t think that your approach with simulatn_ends = 1; will work because of sampling.
I think that you need to set the simulatn_ends = 1; before the end of sim
Ben