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

Hi Doron:

The "least" was not original.  It has been added recently as a part
of moving disable iff to the top level in the formal semantics.

In both Accellera SystemVerilog 3.1a and IEEE Std 1800-2005, we had

  w |= disable iff (b) P iff either w |= P or there exists 
  0 \leq k < |w| such that w^k |= b and w^{0,k-1}\top^\omega |= P.
  Here w^{0,-1} denotes the empty word.


I prefer this simpler definition.  The equivalence with the form with 
"least" is an easy lemma.

J.H.


> X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.21,289,1188802800"; 
>    d="scan'208";a="348567547"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Wed, 17 Oct 2007 11:59:25 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] call to vote on 1757
> Thread-Index: AcgQot6aCoS3akHASOK9mVGvItjgpgAAS2FA
> From: "Bustan, Doron" <doron.bustan@intel.com>
> X-OriginalArrivalTime: 17 Oct 2007 09:59:25.0469 (UTC) FILETIME=[6628CCD0:01C810A4]
> X-eda.org-MailScanner: Found to be clean, Found to be clean
> X-Spam-Status: No, No
> X-MIME-Autoconverted: from quoted-printable to 8bit by server.eda.org id l9HA49Np010094
> Sender: owner-sv-ac@eda.org
> X-eda.org-MailScanner-Information: Please contact the ISP for more information
> X-eda.org-MailScanner-From: owner-sv-ac@server.eda.org
> 
> Hi Johan,
> 
> I do not feel that strongly on that, what do other people think?
> 
> BTW, in the definition of disable iff, the lrm uses the least 
> index that satisfies b.
> 
> Doron
> 
> -----Original Message-----
> From: Johan Martensson [mailto:johan.martensson@jasper-da.com] 
> Sent: Wednesday, October 17, 2007 11:48 AM
> To: Bustan, Doron
> Cc: John Havlicek; Kulshrestha, Manisha; Bassam Tabbara; sv-ac@eda.org
> Subject: Re: [sv-ac] call to vote on 1757
> 
> Hi Doron,
> 
> Omitting the "least index" requirement certainly seems to result in a
> more succinct definition though. From my point of view the purpose of
> formal definitions is not primarily to explain things in an intuitive
> way to users but to provide a tool for investigation of the logical
> connections among properties and so on (something that implementors need
> to do for example), and for this purpose definitions should be as
> succinct as possible, I think.
> 
> Best Reagards,
> 
> Johan
> 
> 
> On Wed, Oct 17, 2007 at 11:17:50AM +0200, Bustan, Doron wrote:
> > Hi Johan
> > 
> > >>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
> > 
> > 
> > I agree about the equivalence but I am not sure whether it is simpler.
> I
> > think it is more intuitive to think of the first b.
> > 
> > Doron
> ------------------------------------------------------------
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
> 
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
> 
> -- 
> 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.