What is the advantage or the main purpose of using Followed by operator in SVA?

SystemVerilog
, ,
1

Hi, Team
What is the purpose of using followed by operator over implication operator? how does they both differ?

Thank you

2

Followed-by operators were later added to the LRM (2009). Quoting from our SVA handbook (Thanks @ben2 @Ajeetha_Kumari_CVC )

the equivalence of sequence_expr #=# property_expr is:
not (sequence_expr |=> not property_expr)

So fundamentally there is a difference - when the ANTECEDENT is false, implication treats it as “vacuous success” while the followed-by throws a failure.

A good application is while writing cover on a property that was using |=> operator - your coverage results would mislead as “covered”, whereas if you use followed-by operator, you would get exactly what you wanted! Below is a tiny example.

module m;
  
  bit clk, a, b;
  
  default clocking dcb @(posedge clk);
  endclocking : dcb
  
  always #5 clk = ~clk;
  
  c_followed_by : cover property (a #=# b) begin
    $info ("c_followed_by pass"); end
    
    c_imp : cover property (a |=> b) begin
      $info ("c_imp pass"); end
     
  a_imp : assert property (a |=> b);
    a_followed_by : assert property (a #=# b);
    
    
  initial begin
    ##10;
    a = 1;
    ##1;
    a = 0;
    b = 1;
    ##10;
    
    ##10 $finish(2);
  end
endmodule : m
1 Like
3

I view the followed-by operator as the concatenation of a sequence followed by a property.

property P_illegal;
 a_sequence ##1 a_property; 
endproperty : P_illegal

property P_legal;
 a_sequence #=# a_property; 
endproperty : P_legal

IEEE 1800-2009 provided the capability of defining a property that follows a sequence by zero or one cycle delay,
starting from the end point of the sequence.
This capability is introduced with the followed-by operators #-# and #=# that concatenates a sequence and a property.

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

1 Like
4

Thank You Srini, i understood the difference when i ran the code.

5

Thanks Ben, I understood the use case where i can use followed by.

6

the both cover statement return the same output at the same time , what is the difference??

7

Here is another discussion on followed-by operator (#-#).

Although I don’t perfectly understand it yet, it doesn’t have meaning of implication (|->). A few articles says “no vacuous pass with followed-by operators, #-#, #=#”. But they are NOT implication property.