For some reason, some of my mails don't seem to get resen't properly by the reflector. I try this with a somewhat different configuration in the CC field. /Johan On Thu, Dec 06, 2007 at 11:01:29AM +0100, Johan Mårtensson wrote: Hi Doron, On Wed, Dec 05, 2007 at 04:21:56PM +0200, Bustan, Doron wrote: > Hi Johan, John, > > I corrected most of Johan's comments. > > There is only the one below. I think I understands this, but it would be good if John could say his opinion. > > >>F.3.1.1 Rewrite rules for sequences. > >>==================================== > >> > >>"The transformation T^s(S,c) recursively defined below produces an > >>unclocked sequence R equivalent to a given clocked sequence S with a > >>leading clock c" > >> > >> Not all clocked sequences according to the abstract syntax (F.2.1) have > >> a leading clock, for example (@(c1)R1)##1(@(c2)R2). However the clock > >> rewrite rules are applicable also in this case by > >> T^s((@(c1)R1)##1(@(c2)R2),1). > > [[DB:]] As far as I understand 16.15 and 16.15.1, in this case c1 is the leading clock. I think there is a difference between the surface syntax where there is from left to right clock flow and the abstract syntax defined in F.2.1. For example consider the surface syntax property @(c1) R1 ##1 @(c2)R2 |-> P1 What is the semantic leading clock for this property? Well according to the rules of 16.15.1 (p.375) it seems it is c1. However P1 will be clocked by c2, as can be inferred from the last example of p. 376. Now if you apply the rewriting T^p(@(c1) R1 ##1 @(c2)R2 |-> P1,c1) using the leading clock c1 as the second argument you will get the following partial result T^s(R1,c1) ##1 T^s(R2,c2) |-> T^p(P1,c1) Note that P1 will be clocked by c1 and not c2 as specified in 16.15.1. This indicates that we need to distinguish clearly between the surface syntax and the abstract syntax as specified in F.2.1 (to which we apply the clock rewriting rules). Therefore we need a translation between surface syntax and abstract syntax in order to be able to apply the clock rewriting rules. For example, the surface syntax formula @(c1) R1 ##1 @(c2)R2 |-> P1 Should be translated into one of the abstract syntax formulas @(c1) (R1 ##1 @(c2)R2 |-> (@(c2)P1)) or @(c1) (R1 ##1 @(c2)R2) |-> (@(c2)P1) or (@(c1) R1) ##1 (@(c2)R2) |-> (@(c2)P1) before clock rewriting is applied. (Actually I think only the last one is legal because of the restriction to non nested clocking in the abstract syntax.) In summary I think we should be clear about that the clock rewriting rules are not applied to the surface syntax but to the abstract syntax. Furthermore as far as I understand the concept of semantic leading clock, it is something that is defined w.r.t. the surface syntax only. In my view it doesn't apply to the abstract syntax at all. Therefore we shouldn't mix the two levels by explaining how to apply the clock rewriting rules in terms of semantic leading clocks. > > > >> > >> In addition according to the (Draft4) abstract syntax for the clocked > >> sequence '@(c) R' R must be unclocked. To apply the rewrite to this > >> clocked sequence would be to evaluate T^s(R,c) or to evaluate T^s(@(c) > >> R,1). Neither of these seem to match with the description. > >> > [[DB:]] I think that T^s(R,c) does match the description. Well the description says T^s should be applied to a _clocked sequence_ S and its leading clock c. So if S=@(c)R, we should compute T^s(@(c)R,c) (which happens to give the same result as T^s(R,c)). Anyway when we recurse down the sequence we will apply T^s to unclocked sequences. I would rather see that we skip all talk of leading clocks here for the reason I gave above, and that we say that T^s is applicable to all sequences of the abstract syntax whether clocked or not. We could for example say the following "The transformation T^s(S,c) recursively defined below produces an unclocked sequence R equivalent to a given sequence S in the context of clock c" Best Regards, Johan > > >> BTW. I hope we have some mantis item for removing the restriction that > >> clocks cannot be nested in the abstract syntax. > > [[DB:]] I agree. I am not sure I know all the details that lead to this restriction. Maybe John knows. > >> > >>Maybe the following could serve as a replacement. > >> > >> "The transformation T^s(S,c) recursively defined below produces an > >> unclocked sequence R equivalent to a given clocked (or unclocked) > >> sequence S in the context of a clock c" > >> > >> > [[DB:]] > I think that for sequences this is not needed. I am not sure about properties of the form "@(c1)p1 or @(c2)p2" > > >>F.3.1.2 Rewrite rules for properties. > >>==================================== > >> > >>Similar comment to that of F.3.1.1 > >> > > Thanks > > 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. -- ------------------------------------------------------------ Johan Mårtensson Office: +46 31 7451913 Jasper Design Automation Mobile: +46 703749681 Kvarnbergsgatan 2 Fax: +46 31 7451914 411 05 Gothenburg, Sweden Skype ID: johanmartensson ------------------------------------------------------------ -- ------------------------------------------------------------ Johan Mårtensson Office: +46 31 7451913 Jasper Design Automation Mobile: +46 703749681 Kvarnbergsgatan 2 Fax: +46 31 7451914 411 05 Gothenburg, Sweden Skype ID: johanmartensson ------------------------------------------------------------ -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Thu Dec 6 05:49:38 2007
This archive was generated by hypermail 2.1.8 : Thu Dec 06 2007 - 05:50:04 PST