[sv-ac] Re: clock rules

Hi Doron:

Something like this should work, but care needs to be taken because
the clock flow depends on parentheses, which may be omitted when
relying on operator precedence.  Annex F does not currently take these
things into account.

For example, the clock flow rules say that a clock does not flow out
of a parenthesized expression, so

  - Flow s(@(c1) (@(c2) S)) =  c2.

should be

  - Flow s(@(c1) (@(c2) S)) =  c1.


The document clock-flow.pdf on mantis 1296 gives draft definitions of
tight satisfaction and property satisfaction with clock flow, and the
notion of what clock flows out of a sequence match is a part of that
definition.  That document does not discuss carefully how the various
inductive cases are chosen in when there is ambiguity in the grammar
due to missing parentheses.  The assumption is that operator
precedence is used and that the overall form is legal to begin with.

By the way, I am not saying that 1932 needs to formalize clock flow.

What I am saying is that 1932 needs to provide a clear intuitive 
description of clock flow in Clause 16 for the new operators, along
the same lines as what is written there already for the old operators.

If we need to study a formalization of clock flow along the lines
suggested by you or by the clock-flow.pdf document, that is fine,
but I am not saying that we have to put these definitions into the LRM
now.

J.H.

> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.20,210,1186383600"; 
>    d="scan'208,217";a="125222296"
> X-MIMEOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Wed, 5 Sep 2007 15:26:35 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: clock rules
> Thread-Index: AcfvuAAaTy0KgtCRQESgvEOJMXuFCw==
> From: "Bustan, Doron" <doron.bustan@intel.com>
> X-OriginalArrivalTime: 05 Sep 2007 12:26:37.0149 (UTC) FILETIME=[00E6B8D0:01C7EFB8]
> 
> This is a multi-part message in MIME format.
> 
> ------_=_NextPart_001_01C7EFB8.00F0AD95
> Content-Type: text/plain;
> 	charset="us-ascii"
> Content-Transfer-Encoding: quoted-printable
> 
> Hi John,
> 
> =20
> 
>  I think I understand your point.
> 
> =20
> 
> The solution should be another inductive function=20
> 
> =20
> 
> - Flow s(@(c) b) =3D  c.
> 
> - Flow s(@(c) (1, v =3D e)) =3D c.
> 
> - Flow s(@(c1) (@(c2) S)) =3D  c2.
> 
> - Flow s(@(c) (S1 ##1 S2)) =3D  Flow(@(Flow(@(c)S1))S2).
> 
> - Flow s(@(c) (S1 ##0 S2)) =3D Flow(@(Flow(@(c)S1))S2).=20
> 
> - Flow s(@(c) (S1 or S2)) =3D if Flow(@(c)S1)=3DFlow(@(c)s2) then
> Flow(@(c)S1) otherwise 0 .
> 
> - Flow s(@(c) (S1 intersect S2)) =3D if Flow(@(c)S1)=3DFlow(@(c)s2) then
> Flow(@(c)S1) otherwise 0.
> 
> - Flow s(@(c) (first match S)) =3D Flow(@(c)S).
> 
> - Flow s(@(c) (S[*0])) =3D c.
> 
> -      Flow s(@(c) (S[*1:$])) =3D Flow(@(c)S).
> 
> =20
> 
> Then,=20
> 
> -      T p(@(c) (S |-> Q) =3D (T s(@(c) S) |-> T p(@(Flow(@c(S)) Q)).
> 
> =20
> 
> With the restriction that Flow(@c(S)) is the only leading clock of Q
> (either because of inheritance or explicitly set)=20
> 
> =20
> 
> Doron
> 
> 

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