SVA: Applications of followed-by operators

Responding to a user query on: https://verificationacademy.com/forums/t/what-is-the-advantage-or-the-main-purpose-of-using-followed-by-operator-in-sva/45808/2

 Followed-by operators were later added to the LRM (2009). Quoting from our SVA  handbook (Thanks Ben Cohen, Ajeetha Kumari & Lisa Piper) 

 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