RE: [sv-ac] new versions of proposals 2173 and 2100 are attached

 
would the following be better ?
 
An evaluation attempt of a property of the form

case (expression_or_dist)

expression_or_dist1 :property_stmt1

...

expression_or_distn : property_stmtn

[ default : property_stmtd ]

endcase

 
is non vacuous iff for some index i such that 1<= i <= n
(expression_or_dist===expression_or_dist_i) and for each index j such
that 1<=j< i (expression_or_dist!==expression_or_dist_j) and the
underlying evaluation attempt of property_stmt_i is non vacuous or
if the default is present and for each index i such that 1<= i <= n
(expression_or_dist!==expression_or_dist_i) and the underlying
evaluation of property_stmt_d is non-vacuous.
 
Yaniv
 

 
________________________________

From: Seligman, Erik [mailto:erik.seligman@intel.com] 
Sent: Monday, March 17, 2008 17:20
To: Fais Yaniv; sv-ac@eda.org
Cc: Bresticker, Shalom; Havlicek John
Subject: RE: [sv-ac] new versions of proposals 2173 and 2100 are
attached


A question/suggestion about 16.14.7h (def of non-vacuity) in 2173: 
is non-vacuous iff either (expression_or_dist===expression_or_dist1) and
the underlying evaluation attempt of property_stmt1 is non-vacuous, or
(expression_or_dist!== expression_or_dist1 && expression_or_dist===
expression_or_dist2) and the underlying evaluation attempt of
property_stmt2 is nonvacuous, or ...,

I think some kind of concise 'For some i,  ' sentence might be cleaner
than the '...' notation here.

 
________________________________

From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Fais Yaniv
Sent: Sunday, March 16, 2008 2:45 AM
To: sv-ac@server.eda.org
Cc: Bresticker, Shalom; Havlicek John
Subject: [sv-ac] new versions of proposals 2173 and 2100 are attached


Hi,
 
I'm attaching (since those Mantis items are in the resolved state and I
can't upload) new versions of the proposals 2173 and 2100
 
They include fixes to feedback from Shalom and John:
 
2100:
 
    (Shalom)
 
        "troughout" -> "throughout"

         "except for it evaluates" -> "except that it evaluates"

2173:

       "I don't think the BNF footnote is needed. Regular cases have the
same restriction with such a  BNF footnote." (Shalom) - I removed the
BNF footnote on more  than one default case, there is a sentence about
this in 16.12.16.

Addressed comments from John:
    1. extra semicolon in assertion statement -A possible solution is to
have both property_spec and          property_statement_spec, where the
former is unchanged, i.e.

        property_spec ::= [clocking_event] [disable iff
(expression_or_dist)] property_expr

        and the latter requires a property_statement in place of the
property_expr.

        Then use property_spec in the assertion statements (unchanged)
and use

        property_statement_spec in the property declaration, getting rid
of the

        explicit semicolon there.

    2. change the definition of vacuity to include n case items with
optional default in one paragraph

    3. change in the multi clocks section (16.15.1) the default to be
optional

 
Yaniv
 
 

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