RE: [sv-ac] 1668 update

Ok, now I see it 

(I should have remember, but I havn't)

Doron

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Monday, August 20, 2007 3:45 PM
To: Bustan, Doron
Cc: john.havlicek@freescale.com; sv-ac@eda-stds.org
Subject: Re: [sv-ac] 1668 update

Hi Doron:

See the proposed changes to Annex F for 1549.  They include the
following:

* w,L_0,L_1 |== (t v; R) iff there exists L such that w,L_0\v,L |== R
  and L_1 = L_0[v] \cup (L\v)

* w,L_0,L_1 |== (1,v=e) iff |w| = 1 and w^0 |= 1 and 
  L_1 = {(v,e[L_0,w^0])} \cup (L_0\v), where e[L_0,w^0] denotes the 
  value obtained from e by evaluating first according to L_0 and
  second according to w^0.  In case w^0 \in {\top,\bot}, e[L_0,\top]
  and e[L_0,\bot] can be any constant values of the type of e.

The new notations are also defined in that .pdf:

  L[v] = L|_{dom(L) \cap v}

  L\v  = L|_{dom(L) - {v}}


I agree that you need to have this definition of tight satisfaction 
to write the proof.

I also needed this definition in order to prove that all the results
in the tecnical report still hold when the syntax (t v; R) is added,
so I thought you had seen it already.

Regarding uniquefying the names, I deleted it from the rewriting 
algorithm because it is not necessary.  I recall highlighting this
as one of the changes.

Please check if you can get your proof to go through with the
definitions above and without any hinting.
 
J.H.  

> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.19,283,1183359600"; 
>    d="scan'208";a="281171905"
> X-MIMEOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Mon, 20 Aug 2007 08:22:29 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] 1668 update
> Thread-Index: AcfisJfMi0KlLXKLTXSK19R0ery6PwAOKFnA
> From: "Bustan, Doron" <doron.bustan@intel.com>
> Cc: <sv-ac@eda-stds.org>
> X-OriginalArrivalTime: 20 Aug 2007 05:22:30.0265 (UTC)
FILETIME=[1AC45E90:01C7E2EA]
> 
> Hi John,
> 
> 
> 
> 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.
> 
> [DB} I don't see how. The flow rules are use to determine the domain
of
> the context not the values of the local variables. So I agree that the
> property is legal, but I am not sure what its semantics is.
> 
> You should also consider this example, which is legal today:
> 
> sequence r;
> logic v;
> (1, v =3D 1) ##1 (v =3D=3D 1);
> endsequence
> 
> property p;
> logic v;
> (1,v =3D 0) ##1 r ##1 (v =3D=3D0);
> Endproperty
> 
> [DB] The rewrite algorithm makes the names unique, so again it is only
a
> hint.=20
> 
> Doron

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