RE: [sv-ac] Clock rewriting rules

Hi John,

Yes, indeed

	@(c) not (Q1 and Q2), where Q1 and Q2 are clocked properties 

cannot be generated from the abstract syntax.

But the syntax itself is legal. Nevertheless, it is not legal either
according the abstract syntax or as a derived form. It looks like we are
inconsistent in any case.

Thanks,
Dmitry

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Monday, June 25, 2007 2:15 PM
To: Korchemny, Dmitry
Cc: sv-ac@eda-stds.org
Subject: Re: [sv-ac] Clock rewriting rules

Hi Dmitry:

Annex F is, and has been for some time, rather delicate.

I think the whole thing should be rewritten along the lines of
suggested in Mantis 1296.  I would prefer to get rid of the 
clock rewriting rules altogether.

Regarding your particular example,

   @(c) not (Q1 and Q2), where Q1 and Q2 are clocked properties

I do not believe that this can be generated from the abstract
syntax.

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.16,455,1175497200"; 
>    d="scan'208,217";a="242586865"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Sun, 24 Jun 2007 09:43:49 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] Clock rewriting rules
> Thread-Index: Ace2KwWTFGI6IbYKS4O1FqHIbUqcVQ==
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 24 Jun 2007 06:43:54.0952 (UTC)
FILETIME=[08B8B480:01C7B62B]
> X-eda.org-MailScanner: Found to be clean, Found to be clean
> X-Spam-Status: No, No
> 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
> 
> This is a multi-part message in MIME format.
> 
> ------_=_NextPart_001_01C7B62B.06053F31
> Content-Type: text/plain;
> 	charset="us-ascii"
> Content-Transfer-Encoding: quoted-printable
> 
> Hi all,
> 
> =20
> 
> Clock rewriting rules are defined in F.3.1 in the following manner:
> 
> =20
> 
> @(c) not P |-->not @(c) P.
> 
> =20
> 
> (other rules are similar),
> 
> =20
> 
> which reads: when the clocking event c is applied to 'not P', where P
is
> an unclocked property, the resulting property is equivalent to not
@(c)
> P.
> 
> =20
> 
> Now let's say that we have the following formula: @(c) not (Q1 and
Q2),
> where Q1 and Q2 are clocked properties. Then, strictly speaking, no
> rewriting rule can be applied, since the above rewriting rule requires
> that Q1 and Q2 were unclocked.
> 
> =20
> 
> I think that a cleaner way would be to define the rewriting rules
using
> a special notation for rewriting transformation as done in PSL:
> 
> =20
> 
> RW(@(c) not Q) =3D not RW(@(c) Q)
> 
> =20
> 
> Note that Q here is a clocked property.
> 
> =20
> 
> What do you think?
> 
> =20
> 
> Thanks,
> 
> Dmitry
> 
> 

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