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
Comments
Post a Comment