SystemVerilog: implies operator vs. |->

Question

Recently the question came up what the difference is between the usual implication operator (|->) and the implies operator in SystemVerilog. Unfortunately I couldn't find a clear answer yet. However, I collected the following information:

From SystemVerilog LRM 1800-2012:

• § 16.12.7 Implies and iff properties:

  property_expr1 implies property_expr2
  A property of this form evaluates to true if, and only if, either property_expr1 evaluates to false or property_expr2 evaluates to true.

• § F.3.4.3.2 Derived Boolean operators:

  p1 implies p2 ≡ (not p1 or p2)

• § F.3.4.3.4 Derived conditional operators:

  (if(b) P) ≡ (b |-> P)

However, the LRM does not really point out what the actual difference is. I assume that they differ in the evaluation in case of a false antecedent (success vs. vacuous success), but I could not find any source or evidence for this assumption. Moreover, I know that the implies operator is very common in combination with formal verification tools like OneSpin.

Could anyone help me out?

P.S.: It seems there is an answer to this question in the following book: SystemVerilog Assertions Handbook, 3rd Edition. But $155 is a bit too much for me just for getting the answer to this question :)

Answer 1

I think there is even a more significant difference. Assume that we have the following example:

property p1;
  @ (posedge clk) 
  a ##1 b |-> c;
endproperty

property p2;
  @ (posedge clk) 
  a ##1 b implies c;
endproperty

assert property (p1);
assert property (p2);

Both implication operators simply have different proving behavior. Property p1 will be triggered through a match of a ##1 b and will look for a matching c during the same clock tick as b. However, property p2 is triggered by a ##1 b and will check for a match of c during the clock cycle of a. This means the properties would pass for the following scenarios:

Property p1 passes and p2 fails: Property p2 passes and p1 fails:

A hint for this behavior can be found in the SystemVerilog LRM. The defined substitutions are:

(if(b) P) = (b |-> P)
p1 implies p2 = (not p1 or p2)

So all in all, if one uses the implies operator it becomes easier to define multi-cycle operations since antecedent and consequence have the same starting point for the evaluation.