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

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