Hi Doron, If I understand correctly this would dispense with the clock rewriting rules altogether. I would prefer a two phase translation instead 1) Surface syntax clocked (clock flow clock scope) ==> abstract syntax clocked (hierarchical clock scope) 2) Abstract syntax clocked ==> abstract syntax unclocked. [Clock rewriting] The relation to clocking in PSL would be more evident, I think. Best Regards, Johan On Tue, Dec 11, 2007 at 05:36:04PM +0200, Bustan, Doron wrote: > 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. -- ------------------------------------------------------------ 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 Wed Dec 12 16:20:12 2007
This archive was generated by hypermail 2.1.8 : Wed Dec 12 2007 - 16:20:55 PST