4

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.

AndresM
  • 1,293
  • 10
  • 19
vivek M
  • 41
  • 1
  • 1
  • 2

3 Answers3

2

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.

Barett
  • 5,826
  • 6
  • 51
  • 55
dave_59
  • 39,096
  • 3
  • 24
  • 63
2

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

Refer to IEEE Std 1800-2012 ยง 16.12.6 Implication

Greg
  • 18,111
  • 5
  • 46
  • 68
0
  • 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

abhay chavda
  • 1
  • 1