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.