Re: [sv-ac] call to vote on 1757

Hi,

I vote no to AcceptRejecton1757.071122.pdf  because I think we need to
discuss the precedence of the abort operators relative to the others a
little more. Following our discussion at Tuesday's meeting I see no
reason why the abort operators should have higher precedence than |->,
|=>, and if..else. I think users will find it intuitive that everything
to the right of the abort operator (with boolean) will be aborted.

As far as I understand if the abort operators are given higher
precedence than |-> then for example 'accept_on (c) a|->b'  will be a
syntax error because it will parse as '(accept_on (c) a)|->b' and
'(accept_on (c) a)' is a property_expr which is disallowed at the LHS of
|->.

In PSL the abort operator has higher precedence than many of the
property level (FL) operator, but (as I mentioned in our previous
meeting), that makes sense because this operator is postfix. 

If the PSL abort operator would have had lower precedence that the |->
operator then '{a}|->{b} abort c' would have parsed as '({a}|->{b})
abort c' wheras the user probably has '{a}|->({b} abort c)' in mind.
Similar considerations seem to be applicable in relation to PSL
eventually!, until, always, never etc. which have lower precedence than
abort in PSL.

Furthermore I think the SVA abort operators can be safely placed beneath
the 'if..else' operator since, I don't think the relative precedence of
these operators has any impact on the parsing of either 'accept_on (a)
if (b) then P else F' or 'if (b) then accept_on (a) P else accept_on (a)
F'

I also have some friendly amendments:

16.12.3

I think 'semantics' is in the singular in this context.
REPLACE
The semantics of reject_on(expression_or_dits) property_expr are the
same as not(accept_on(expression_or_dist) not(property_expr)).
WITH
The semantics of reject_on(expression_or_dits) property_expr is the
same as not(accept_on(expression_or_dist) not(property_expr)).

16.12.3 Abort properties

The first and second example are duals but the explanations are slightly
different. The first states "the truth of p1 is ignored in deciding the
truth of p", and the second one says "then the second term is ignored in
deciding the truth of p". I think both should be explained in the same
way otherwise some may think there is some essential difference.

For example (explanation to the first example.)
REPLACE
If a becomes true during the evaluation of p1, the truth of p1 is
ignored in deciding the truth of p  On the other hand, if b becomes true
during the evaluation of p2 then p evaluates to false. 
WITH
If a becomes true during the evaluation of p1, then the first term is
ignored in deciding the truth of p  On the other hand, if b becomes true
during the evaluation of p2 then p evaluates to false. 

Best Regards,

Johan


On Tue, Nov 20, 2007 at 02:52:00PM -0600, John Havlicek wrote:
> Hi Folks:
> 
> This is the call to vote on the proposal for Mantis 1757.
> 
> The document on Mantis is 
> 
>    AcceptRejecton1757.071107.pdf
> 
> Please vote if you are eligible.  See the details below.
> 
> J.H.
> 
> ----------------------------------------------------------------------------------
> Ballot on Mantis 1757
> 
> - Called on 2007-11-20, final ballots due by 2007-11-26 T 23:59-08:00.
> 
>  v[xxxxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel)
>  v[-xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys)     
>  n[----------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys)
>  v[xx-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale)
>  t[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair)
>  v[xxxxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair)
>  v[xxxxxxxxx-xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor Graphics)
>  n[------------------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics)
>  n[---x------------x--xxx.....................] Joseph Lu (Altera)
>  v[xxxxxxxxxxxxx..............................] Johan Martensson (Jasper)
>  n[---------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale)
>  v[xxxx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence)
>  v[xx-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel)
>  n[-x-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics)
>  v[-x-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys)
>  v[xxx-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems)
>    |------------------------------------------- attendance on 2007-11-20
>  |--------------------------------------------- voting eligibility for this ballot
> |---------------------------------------------- email ballots received
> 
>         Legend:
>                 x = attended
>                 - = missed
>                 r = represented
>                 . = not yet a member
>                 v = valid voter (2 out of last 3 or 3/4 overall)
>                 n = not a valid voter
>                 t = chair eligible to vote only to make or break a tie
> 
> 
> -- 
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.

-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Arvid Hedvalls backe 4           Fax: +46 31 7451939
411 33 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.