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