Difference between -> and => in assertions

SystemVerilog
1

difference between : sig_a - > ##2 sig_b and sig_a = > ##2 sig_b in systemverilog assertions

2

→ immediately evaluated
=> next clock cycle evaluated
=> is equal to ->##1

u can say sig_a=>##2 sig_b as sig_a ->##3 sig_b

1 Like
3

To write a constraint that sig_a goes high, sig_b must follow within 3 clk cycles.

sig_a |-> [1:3] sig_b; // is this correct

4

Be careful with your syntax

  • A -> B is a logical implication operator equivalent to !A || B
  • A |-> B is an overlapping implication property operator. When A and B are both boolean expressions, it behaves the same as the logical operator, except that !A is considered a vacuous success.
  • A |=> B is non-overlapping implication property operator. It is equivalent to A|-> ##1 B. We recommend using the latter for consistency and clarity.
  • A -> ##[1:3] B means B must follow between 1 and 3 cycles.
1 Like
5

Hi Dave,

I believe this is incorrect. The ##1 1 should be part of antecedent in the equivalent expression

As per LRM Section 16.12.7 Implication

sequence_expr |=> property_expr
is equivalent to the following:
sequence_expr ##1 `true |-> property_expr
6

It’s true that there can be a subtle difference in some cases. However, in most instances, there’s no difference.