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

Hi,

W.r.t. (3) below neither do I understand the sentence in question, nor
do I understand how the sentence could be interpreted such as to express
a difference to disable iff.

I have another comment:

It seems to me that 

w^{0..i-1}T^\omega|=P for i the least index,0 < i < |w|, such that w^i|=b,

and 

w^{0..i-1}T^\omega|=P for some i,0 < i < |w|, such that w^i|=b

are eqiuvalent.

The reason for this is that if i<=j and

w^{0..j}T^\omega|=P

then

w^{0..i}T^\omega|=P

This means that we can simplify the semantic definition to

  w|= accept_on (b) P iff 
  
   w|=P 
  or 
   w^{0..i-1}T^\omega|=P for some i,0 < i < |w|, such that w^i|=b

or equivalently

   w|=P 
  or 
   there exists i such that 0 < i < |w| and w^i|=b and w^{0..i-1}T^\omega|=P

Best Regards,

Johan

On Tue, Oct 16, 2007 at 06:21:45PM -0700, Bassam Tabbara wrote:
> Agreed on (5), good catch Manisha, we need new op types in note (2) for
> the accept_on/off in 36.45. I think we can choose to spawn off a mantis
> item (properly added on CC's workload with immediate priority) albeit I
> personally would rather keep things together to avoid missing (near miss
> this time :)!) and then request review by CC.
> 
> Thx.
> -Bassam.
> 
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
> Kulshrestha, Manisha
> Sent: Tuesday, October 16, 2007 3:03 PM
> To: john.havlicek@freescale.com; sv-ac@eda.org
> Subject: RE: [sv-ac] call to vote on 1757
> 
> Hi,
> 
> I vote no on 1757. I think the following issues need to be addressed:
> 
> 1) In the proposal it has:
> 
>  h) A property is a reset if it either of the form
> 
> accept_on(expression_or_dist) property_expr
> or of the form
> reject_on(expression_or_dist) property_expr
> 
> I think this part needs some grammar change. 
> 
> 2) In the propel it says "Insert 16.12.3" but it does not say what would
> be the title of this clause.
> 
> 3) In the same section "16.12.3" it says "accept_on affects the truth of
> a property in its scope.". I do not quite understand this sentence. 
> 
> 4) I am just wondering if there would be any confusion in calling the
> expression in accept_on or reject_on as reset expression. We call the
> expression in disable iff as reset expression and its semantics is
> different than the semantics of these new properties.
> 
> 5) I think some changes in 36.45 will be required due to these new
> property types.
> 
> Thanks.
> Manisha
> 
> -----Original Message-----
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
> Behalf Of John Havlicek
> Sent: Wednesday, October 10, 2007 6:54 PM
> To: sv-ac@server.eda.org
> Subject: [sv-ac] call to vote on 1757
> 
> Hi Folks:
> 
> This is the call to vote on Mantis 1757.  The document in Mantis is
> 
>   Accept_reject_on.1757.07.09.25.pdf
> 
> Please vote if you are eligible.  See details below.
> 
> J.H.
> 
> ------------------------------------------------------------------------
> -------------------
> 
> Ballot on Mantis 1757
> 
> - Called on 2007-10-10, final ballots due by 2007-10-17 T 23:59-07:00.
> 
>  v[xxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel)
>  v[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys)     
>  n[----------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys)
>  v[xxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale)
>  t[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale -
> Chair)
>  v[xxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel -
> Co-Chair)
>  v[xxx-xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor
> Graphics)
>  n[------------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics)
>  n[----------x--xxx.....................] Joseph Lu (Altera)
>  v[xxxxxxx..............................] Johan Martensson (Jasper)
>  n[---------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale)
>  v[xxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence)
>  v[x-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel)
>  n[--x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics)
>  v[xxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys)
>  v[xxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun
> Microsystems)
>    |------------------------------------- attendance on 2007-10-09
>  |--------------------------------------- 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.
> 
> 
> -- 
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 
> 
> 
> -- 
> 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.