Search code examples
system-verilog-assertionsimplication

What is the difference between the symbol '->' and '|->' in System Verilog Assertion Properties

I have encountered an example property which works here:

property p_a;
    @(posedge clk) $rose(a) -> $rose(b);
endproperty

There is no syntax error above.

Then I tried to modify to this

property p_a;
    @(posedge clk) $rose(a) -> ##2 $rose(b);
endproperty

Which gives me syntax error, only to realize its not actually '|->'

property p_a;
    @(posedge clk) $rose(a) |-> ##2 $rose(b);
endproperty

This works, so what is the symbol -> actually here in property? I know usually its for triggering an event.

Solution

  • The -> operator is a logical implication operator, works on the logical operands:

    The logical implication expression1 –> expression2 is logically equivalent to (!expression1 || expression2)

    The |-> is a sequential implication used to express certain temporal properties.

    The implication construct specifies that the checking of a property is performed conditionally on the match of a sequential antecedent ... This construct is used to precondition monitoring of a property expression and is allowed at the property level. The result of the implication is either true or false. The left-hand operand sequence_expr is called the antecedent, while the right-hand operand property_expr is called the consequent...

    In other words, the first one is can be used for logical functions, the second is used in sequences of events. They are very much different.