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

Hi Ben:

My question is really just about the naming of the buckets. The
familiar convention I have is that at the top level there are three
buckets: PASS, FAIL, DISABLE. Then the PASS bucket divides into
VACUOUS PASS and NONVACUOUS PASS.

What you seem to be saying is that you want PASS to mean NONVACUOUS and
have a VACUOUS PASS be the other bucket.

This just seems a naming question, and I'm not sure what the vendor
intended for the names.

J.H.

From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Tuesday, July 13, 2010 10:14 AM
To: Havlicek John-R8AAAU
Cc: sv-ac@eda.org
Subject: Re: [sv-ac] Re: Question on vacuous success

John,

 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.

Thus, for the following case:

 logic a=1, b=0, c;
     ap_abc: assert property(@ (posedge clk) a|-> b |-> c);

ap_abc is vacuous when a==1, b==0, c;

In the assertion report, that vendor provides a failure count and a pass
count.

It would be an error (IMHO) if the pass count is incremented under those
conditions.

Note that vacuous assertions are not reported in the pass count. That
vendor did it correctly for the case of

ap_bc: assert property(@ (posedge clk) b |-> c); // when b==0

Ben

On Tue, Jul 13, 2010 at 4:49 AM, Havlicek John-R8AAAU
<r8aaau@freescale.com> wrote:

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.