Subject: Re: [sv-ac] Draft of SVAC ballot for 2/24
From: Stephen Meier (Stephen.Meier@synopsys.com)
Date: Sun Feb 23 2003 - 12:01:39 PST
Cindy:
Thanks for your comments.
At 02:38 PM 2/23/2003 +0200, Cindy Eisner wrote:
>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".
Since you were the proposer of the issue, I suggest that we just withdraw
#3 and instead place #13 "change never syntax to not" onto the ballot as
it seems to have strong support and would make things consistent.
>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.)
Yes, let's further consider the semantics of the directives in procedural
context
and determine what restrictions are appropriate. Note that we have not really
considered whether assertions are appropriate inside of initial blocks. My
initial
inclination is to not allow this as to not place the burden on formal tools
to conduct
this processing as initial blocks are mostly part of simulation semantic
and not
necessarily part of the design. I would lean to having procedural
assertions have
an implied always and put a restriction that 'initial' cannot be used in
procedural context.
>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
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 - 12:02:26 PST