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

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

Thank you

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

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
    a = 1;
    a = 0;
    b = 1;
    ##10 $finish(2);
endmodule : m
1 Like

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
Link to the list of papers and books that I wrote, many are now donated.

1 Like

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

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