SVA: Use the |=> or the |-> ##1?

SystemVerilog
1

I generally prefer to use the overlapping implication operator |-> ##1 or with the ##[1:static_range] because it read better. The (antecedent |-> ##1 sequence) reads as:
if(antecedent_is _a_match) then AT the next cycle the sequence is checked.
However, The (antecedent |=> sequence ) reads as:
if(antecedent_is _a_match) then starting from the next cycle the sequence is checked
For example:
a |-> ##[1:4] b; // reads
“if(a) then in cycles 1 to 4 , after the antecedent match, b==1”
a |=> ##[0:3] b; // reads
“if(a) then starting from the next cycle, after the antecedent match, to the next 3 cycles from that ‘next’ cycle b==1.
Note the change in range [0:3] instead of [1:4] because with the |=> we are at the next cycle.
The non-Overlapped Implication Operator |=> requires (IMHOP) a mental effort to go through the conversion of what this |=> is. Speaking of which,

sequence_expr |=> property_expr // is equivalent to:
sequence_expr ##1 `true |-> property_expr

// The above definition is important to understand because
sequence_expr ##1 `true |-> property_expr // LEGAl but different than
sequence_expr |-> ##1 property_expr // ILLEGAL
(##1 property) // is NOT a property

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers: