RE: [sv-ac] Mantis 0001381: vacuous success is not well defined in the LRM

Doron,
OK what will be reported is tool dependend but if LRM defines vacuous
success then IMHO this is interesting debug info for user to see/count the
vacuous successes.
My problem is vacuous vs property operators and yours responce is very
unclear to me in context of mantis 1381which says : " an evaluation attempt
of a property of the form not property_expression is non-vacuous iff the
underlying evaluation of property_expression is non-vacuous"
Regarding to above in case 2 the result should be vacuous not as you claim
fail. 
Question is which action block shuold be executed for both cases.
 
IMHO there may be two interpretation : we have 3-state assertion outcome
(Fail, PASS, VACUOUS PASS) or 4-state (PASS, FAIL, VACUOUS PASS, VACUOUS
FAIL). Both of them have flaws. 3state - we dont know which action block
should be triggered, 4state mantis 1381 do not define true tables for
4states.
 
DANiel


  _____  

From: Bustan, Doron [mailto:doron.bustan@intel.com] 
Sent: Wednesday, November 21, 2007 4:10 PM
To: danielm; sv-ac@server.eda-stds.org
Subject: RE: [sv-ac] Mantis 0001381: vacuous success is not well defined in
the LRM



Hi Daniel,

 

We didn't envision reports of vacuous attempts. The way I see it, the things
that need to be reported are

1.	Assertions failures. In your example it is the second case. 

2.	Non-vacuous successes. None of the cases in you example are
non-vacuous successes. 

Non-vacuous successes should be considered as coverage hits, meaning you
expect at least one simulation 

In which at least one attempt is non-vacuous.

 

Regards

 

Doron

 

  _____  

From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of danielm
Sent: Wednesday, November 21, 2007 4:52 PM
To: sv-ac@server.eda-stds.org
Subject: [sv-ac] Mantis 0001381: vacuous success is not well defined in the
LRM

 

Maybe my 1st question was too abstarct - lets start with smth simpler: we
have a=0 and b=1 on (posedge clk) event.

 

Case 1:Which action block should be executed (a|->b outcome is vacuous pass)

    assert property (@posedge clk) a|->b) $display("pass") else
$display("fail");

 

 

Case 2:Which action block should be executed (a|->b outcome is vacuous pass)
in below case 

    assert property (@posedge clk)not ( a|->b)) $display("pass") else
$display("fail");

 

 

Should attempt be reported as vacuous for both above?

 

Lets just think how it should for other nested operators.

 

DANiel

 

  _____  

From: danielm [mailto:danielm@aldec.com.pl] 
Sent: Tuesday, November 20, 2007 4:48 PM
To: 'sv-ac@server.eda-stds.org'
Subject: 0001381: vacuous success is not well defined in the LRM

This mantis item is describing how should vacuous matches be evaluate with
property operators.

 

The problem is that it is stil unclear for me if there is vacuous success
and vacuous failure or there is only vacuous succeses. 

 

Let see the example:

 

module top;
        reg clk;

        reg a=0,b=1;

 

        initial begin
                #1;
                clk=1;
                #1;
        end

 

        as1:assert property (@(posedge clk)not a |-> b) $display("not
pass"); else $display( "not fail");
        as2:assert property (@(posedge clk) a |-> b) $display(" pass"); else
$display( " fail");

 

endmodule

In above case a|->b at posedge clk has vacuous pass. So according to
proposal ("an evaluation attempt of a property of the form not
property_expression is non-vacuous iff the underlying evaluation attempt of
propert_expression is non-vacuous")  not a|->b should also be vacuous, but
vacuous what? fail. Which action block for as1 should be executed.

 

If we accept 4-value assertion outcome (Fail F, Pass P, Vacuous Pass VP,
Vacuous Fail VF) then all rules for operators should be defined for 4 values
- in proposal they are defined for three values (Fail, pass, vacuous pass)

Lets see how it should look like for or operator:

 

or         | P     | VP     | F     | VF

P         | P    | P    | P    |    P

VP       | P    | VP    | F    |    VP

F         | P    | F    | F    |    F   

VF     | P    | P    | F    |    VF

 

I dont understand why the proposal doesn't describe behaviour for all
posiible assertion outcomes.

 

DANiel


-- 
This message has been scanned for viruses and 
dangerous content by  <http://www.mailscanner.info/> MailScanner, and is 
believed to be clean. 

---------------------------------------------------------------------

Intel Israel (74) Limited



This e-mail and any attachments may contain confidential material for

the sole use of the intended recipient(s). Any review or distribution

by others is strictly prohibited. If you are not the intended

recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and 
dangerous content by  <http://www.mailscanner.info/> MailScanner, and is 
believed to be clean. 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.