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.