RE: [sv-ac] Question on vacuous success

Hi Ben:

I think that you want to collect non-vacuous pass coverage rather than
create an auxiliary sequence on which to collect coverage.

J.H.

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben
cohen
Sent: Saturday, July 10, 2010 2:05 AM
To: sv-ac@eda.org; Korchemny, Dmitry
Subject: [sv-ac] Question on vacuous success

Dmitry,

If I have the following (attached file)

 logic a=1, b=0, c;

  ap_abc: assert property(@ (posedge clk) a|-> b |-> c);

  ap_bc: assert property(@ (posedge clk) b |-> c);

We agree that the property (b |-> c) succeeds vacuously.

Question: If a vendor states the following in the assertion report, is
he in error, per LRM in claiming ap_abc as a PASS,

yet ap_bc as NO pass? I understand that if b==0 the property b |-> c
is vacuously true, which in essence is true.

But in my mind, it is not a true success, thus, a PASS count of 1 is
misleading.

I guess we need the cover of the sequence a ##0 b ##0 c

ASSERTION RESULTS:

-------------------------------------------------------

Name File(Line) Failure Pass

                                          Count Count

-------------------------------------------------------

/top/m1/ap_abc test_if.sv(25) 0 500

/top/m1/ap_bc test_if.sv(26) 0 0

-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , and is
believed to be clean. 
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.