what is the difference between -> and => in system verilog assertions?

3
votes

I wanted to know when to use -> and => in SVA ? Are there any differences between 

sequence A;
 req |-> ##1 gnt;
endsequence

and 

sequence B;
 req |=> ##1 gnt;
endsequence

Please let me know.. Thank you.

3
system-verilogassertionssystem-verilog-assertions

3 Answers

2
votes

The difference is when the antecedent (the expression on the left) succeeds, does the consequent (the expression on the right) start on the same clock cycle |-> (overlapping) or the next clock cycle |=> (non-overlapping).

A handy way to remember this is there is only one bar in -, so that is overlapping. And there is are two bars in =, so that is non-overlapping.

2
votes

|=> is equivalent to |-> ##1
Therefore, req |=> ##1 gnt; is equivalent to req |-> ##2 gnt;

Refer to IEEE Std 1800-2012 ยง 16.12.6 Implication

0
votes
  • This both kind of implication operator use below type of methodology..
  • I think you got the basic idea of where to use |->(overlapping) and |=>(Non overlapping)

property name(); Enabling sequence (|-> or |=>) Consequent sequence endproperty

Result :

  • when enabling sequence is 'true (1'b1) than it checks consequent sequence ..if consequent seq is 'true than assertion passes and if consequent seq is 'false than assertion fails..

  • When enabling seq is `false than it pass but gives display as "viscus success" and you won't able to see green arrow in waveform

while...

property name(); sequence1 (## delay) sequence2 endproperty

  • In this case if seq1 is 'true than after some delay it checks seq2 if seq2 is `true than assertion pass and if seq2 is 'false than assertion fails..
  • If seq1 is `false than assertion fails directly..

This is main difference of this things..I think it might help