-> operator in the middle of a property

Question

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 is true? Does it behave like an overlapping implication operator? Please see the example below. Thanks.

property count_event(reg [15:0] PerfCtr, reg [15:0] event_count);

 
@(posedge DfiClk)

disable iff (disable_perfcntcheck)

((PWR_OK === 1'b1) && (Reset === 1'b0) && (DebugPerfCtrEn === 1) && (dfi_event_select === 1) && ($rose(dfi_event))) |->

##[1:5] !$isunknown(capture_dly) && (**!capture_dly -> event_count == PerfCtr**) ##1 !$isunknown(capture_dly) && (**capture_dly -> event_count == PerfCtr**);

Answer 1

It looks like it is in the middle of a logical expression, not property. It is the logical implication operator:

11.4.7 Logical operators

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.