Re: [sv-ac] 1668 update

Hi Doron:

The syntax

  (t v [=e]; r)

  (t v [=e]; p)

exists only in Annex F.  The declaration you show is not enabled
by the proposal.

I think it will be good to allow this in the future.  It will
make local variables first class.  If this is done, then the 
scope of a local variable declared in this way has to match
what is in Annex F.

I think that you should be able to prove the expected semantics
of your property using the new flow rules.  I don't think it
is a matter of hinting.

You should also consider this example, which is legal today:

sequence r;
logic v;
(1, v = 1) ##1 (v == 1);
endsequence

property p;
logic v;
(1,v = 0) ##1 r ##1 (v ==0);
endproperty

J.H.

> X-Authentication-Warning: server.eda-stds.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.19,280,1183359600"; 
>    d="scan'208";a="265092986"
> X-MIMEOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Sun, 19 Aug 2007 09:01:52 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] 1668 update
> Thread-Index: Acfho3pI9rf9nsx4Seu7nMdn2z5lTgAgYFkg
> From: "Bustan, Doron" <doron.bustan@intel.com>
> X-OriginalArrivalTime: 19 Aug 2007 06:01:53.0010 (UTC) FILETIME=[70A8E520:01C7E226]
> 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-stds.org id l7J62MZq002935
> 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 John,
> 
> Do we really want to support this type of property?
> 
> property p;
> 
> logic v;
> 
> (1,v = 0) ##1 (logic v; (1, v = 1) ##1 (v == 1)) ##1 (v ==0);
> endproperty
> 
> Although the flow rules hint that this property holds in every
> computation (weak semantics), it does not say so explicitly. If we do
> want to support it we should define scope rules. If not, we should
> forbid declaring the same local variable twice in the same
> property/sequence.
> 
> Doron
> 
> -----Original Message-----
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
> Behalf Of John Havlicek
> Sent: Saturday, August 18, 2007 5:21 PM
> To: sv-ac@server.eda-stds.org
> Subject: [sv-ac] 1668 update
> 
> Hi Folks:
> 
> I have good news about 1668.  I got the intuition last Monday
> that introducing the parenthesized, scoped local variable 
> declarations to the abstract syntax should be able to give
> us a good solution for local variable declaration assignments
> even for sequences that admit empty match.
> 
> I have spent a lot of time this past week working out the
> theory for this, and it looks very good to me.  I have attached
> my plain text notes, which I will also put on mantis.
> 
> I intend to revise the proposal documents to remove the restriction
> disallowing empty match, one which I have never liked.
> 
> I also introduced a formal definition of admits_empty at the
> level of the abstract syntax to address Dmitry's concerns.  I 
> carried out the proof that this definition faithfully represents
> at that level the notion of admitting tight satisfaction by the
> empty word after local variable declaration assignments and
> clocks are eliminated.  This was not as easy as I had hoped, but
> maybe the proofs can be simplified.
> 
> Please have a look and send any feedback that you have.
> 
> J.H.
> 
> -- 
> 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.