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

John,
< at the top level there are three buckets: PASS, FAIL, DISABLE.>
Actually, I see 4 buckets for the fate of an assertion: Success (i.e., holds
vacuously or non-vacuously), Fail, disabled, killed (with the $assertkill).

<What you seem to be saying is that you want PASS to mean NONVACUOUS and
have a VACUOUS PASS be the other bucket. >
Yes. I see vacuous true and non-vacuous pass.
This might be mentioned in the lrm, but vendors report the count for
non-vacuous
passes and the count for failures.
Also, in the simulation traces for assertions, they distinguish the two
types of true with different symbols.
In my mind, a pass is a true, non-vacuous termination, and a termination of
true vacuously.
Ben

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

> 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.