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

I see a similar discussion in 16.14.3, which indicates that two assertion expressions are equivalent (although it's in context of multi-clock properties):

Clock flow also makes the adjointness relationships between concatenation and implication clean for
multiclocked properties:
@(c) x ##1 y |=> @(d) z
is equivalent to
@(c) x |=> y |=> @(d) z
and
@(c) x ##0 y |=> @(d) z
is equivalent to
@(c) x |-> y |=> @(d) z

Warm regards,
Tapan
"You must be the change you want to see in the world" : Mahatma Gandhi
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben cohen
Sent: Tuesday, July 13, 2010 8:44 PM
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<mailto: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> [mailto: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<mailto: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<mailto: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<http://test_if.sv>(25) 0 500
/top/m1/ap_bc test_if.sv<http://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<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.