[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, and is
believed to be clean.