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

 

  _____  

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