Hi Johan, John, I completely forgot about 1296 (shame on me.) Johan, I think the proposal would have fix the problem that you described. Should I add it to 1932? It is not that much work and I think it is in good condition (some adjustment to 1549 is needed to the local variables part), but I am afraid that reviewing time will become even longer, and it is already far too long. Doron >>-----Original Message----- >>From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On >>Behalf Of Johan M?rtensson >>Sent: Thursday, December 06, 2007 12:01 PM >>To: Bustan, Doron >>Cc: john.havlicek@freescale.com; sv-ac@server.eda.org >>Subject: [sv-ac] Re: 1932: Review of LTL_Formal.071120.pdf >> >>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 >>------------------------------------------------------------ >> >>-- >>This message has been scanned for viruses and >>dangerous content by MailScanner, and is >>believed to be clean. --------------------------------------------------------------------- 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. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Wed Dec 12 16:10:48 2007
This archive was generated by hypermail 2.1.8 : Wed Dec 12 2007 - 16:12:01 PST