RE: [sv-ac] Re: Question on vacuous success

Hi Ben:

I am missing the point of why "PASS" is interpreted to mean "NONVACUOUS
PASS"? Is this what the tool documentation tells you?

J.H.

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben
cohen
Sent: Sunday, July 11, 2010 9:14 PM
To: sv-ac@eda.org; Korchemny, Dmitry
Subject: [sv-ac] Re: Question on vacuous success

Per LRM 16.15.8 Nonvacuous evaluations

h) An evaluation attempt of a property of the form sequence_expression
|-> property_expr is nonvacuous

if, and only if, there is a successful match of the antecedent
sequence_expression and the evaluation

attempt of property_expr that starts at the end point of the match is
nonvacuous.

An evaluation attempt of a property of the form sequence_expression |=>
property_expr is nonvacuous

if, and only if, there is a successful match of the antecedent
sequence_expression and the evaluation

attempt of property_expr that starts at the clock event following the
end point of the match is

nonvacuous.

Thus, in my example, I believe that it is an error for a simulator to
report a PASS (true success) if in (a |-> property) the antecedent has
a successful match and the consequent is a property that is vacuuous.

On Sat, Jul 10, 2010 at 12:05 AM, ben cohen <hdlcohen@gmail.com> wrote:

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.