I understand that [-> m] is a non-consecutive GoTo operator and can be used as (e.g.)
@(posedge clk) a |=> b [->2] ##1 c;
But I came across an example, where I see (in the middle of a property), a → b. What does that mean? Does it mean if a is true that b should be true? Does it behave like an overlapping implication operator? Please see the example below. Thanks.
In reply to a72:
Per 1800’2017 The logical implication expression1–> expression2 is logically equivalent to (!expression1 || expression2), and the logical equivalence expression1 <–> expression2 is logically equivalent to ((expression1–> expression2) && (expression2–> expression1)). Each of the two operands of the logical equivalence operator shall be evaluated exactly once.
Thus,
a |-> b-> c; // states
// if(a==0) the property is vacuously TRUE
// If(a==1) the consequent is evaluated and must be true for a true assertion
// Note that there is in assertions vacuity, vacuous true or nonvacuous true
// A consequent that is a sequence is never vacuous.
// For the consequent to be true either one of these 2 conditions
// if(b==0) the expression is TRUE (no vacuity in expressions, only in assertions)
// if(c==1) the expression is TRUE
//Thus, if you think about it, there is a sort of parallelism in thoughts
// in the logical implication and the property implication.