Hi all:
When I amusing SVA, I am a little confused in assertion coverage.
In the following example, how to check both if and else branches are covered.
property p_if_else;
@(posedge clk)
($fell(start) ##1 (a || b)) |->
if(a)
(c[->2]) ##1 e)
else
(d[->2]) ##1 f)
endproperty
Anthother example, how to check both b, c, d are covered
property p_exp;
@(posedge clk)
(a)|-> (b || c || d);
endproperty
Can anyone help me, thanks in advance.
In reply to hungtaowu:
The way SVA is defined, any non-vacuous pass of an assertion is considered “covered”. You will have the same issue with a range in a sequence. If you have requirements that each condition be tested, you need to separate the properties.
In reply to dave_59:
In reply to hungtaowu:
The way SVA is defined, any non-vacuous pass of an assertion is considered “covered”. You will have the same issue with a range in a sequence. If you have requirements that each condition be tested, you need to separate the properties.
Thank you, dave. You’ve really been a big help.