Re: [sv-ac] Draft of SVAC ballot for 2/24


Subject: Re: [sv-ac] Draft of SVAC ballot for 2/24
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Sun Feb 23 2003 - 04:38:57 PST


steve,

a couple of comments on the ballot:

1. comment on #3

>>Is voting against #3 also voting against replacement of 'never' with
'not' ?
>
>No. 'never' has always really meant 'not' and I'm happy to see the
>semantics group correct this incorrect name.

i proposed #3 thinking that "never" meant "never", and i thought we were
going to vote on it under that assumption. in light of the above, and in
light of the note you included on the ballot regarding #3 ("note that
semantics group has unanimously reccomended that never keyword be changed
to not to conform with its semantic description") it seems that #3 should
now read:

Do not allow initial and not to co-occur as directives.

thus, the justification for #3 no longer exists, in my opinion. so, my
recommendation as the original proposer of #3 is to vote "no".

2. comment on #4

in light of the bnf you have written for #4, and in light of thursday's
presentation on embedding assertions in procedural code, i would like to
clarify:

the intention was that at the top level an assertion must have an explicit
"always" or "initial". i was not thinking of embedding in procedural code
(sorry, i know that's the whole point of this committee, but since it
didn't appear in revision 0.79, it slipped my mind). so i would like to
modify the ballot to make this clear as follows:

independent of other syntax issues the bnf would be something like:

prop_spec ::=
             ['initial' | 'always'] ['accept' '(' expression ')' ] ['not']
clocked_expr
                     | identifier ['(' expression_list ')']

then, a semantic restriction would be that when not embedded in procedural
code, one of either "initial" or "always" must appear. finally, the
extraction would add either "initial" or "always" when the assertion is
extracted from an initial or an always block, respectively. (and thus if
the user coded either "initial" or "always" for an embedded assertion, she
would end up with two of either "initial" or "always" which would be an
error.)

regards,

cindy.

Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-8296-114
Haifa 31905, Israel e-mail:
eisner@il.ibm.com

Stephen Meier <Stephen.Meier@synopsys.com>@eda.org on 21/02/2003 09:43:08

Sent by: owner-sv-ac@eda.org

To: sv-ac <sv-ac@eda.org>
cc:
Subject: [sv-ac] Draft of SVAC ballot for 2/24

Hi:

Please review ballot and provide any feedback by 12noon Sunday at which
point I will publish the final ballot by Sunday night and votes will be due
by Monday 9pm Pacific.

Steve

Steve Meier (stephen.meier@synopsys.com) W: 650-584-4476, Cell:
408-393-8246



This archive was generated by hypermail 2b28 : Sun Feb 23 2003 - 04:36:22 PST