Hi Doron, At least I have a hard time understanding that passage although unlike many prospective readers I understand in advance what you are trying to say. Let me go through the text, sentence by sentence in order to explain more in detail why I find it hard to comprehend: > "Given a simulation run w, a sequence s may have multiple matches over > prefixes of w. This seems to be a good introduction stating a general fact about sequence matching. > Furthermore, even if there is no prefix of w that matches s, it could > be that every prefix has the potential to match s in the future in > multiple ways. This sentence is only relevant for weak embedding as far as I understand, but that is not stated. The reader has to find that out for himself. Furthermore the semantic terminology here is different from that of the explanation of the semantics of weak embedding two sections above. There it is explained in terms of "there is no finite prefix that witnesses a non-match of the sequence.", here again it is referred to in terms of "every prefix has the potential to match s in the future". Two different semi technical terms "witnessing a non-match" and "has the potential to match" are introduced without any explanation of their relation. I think it would help understanding if we would stick to the terminology that was introduced initially, or chose one and stick to it. I suspect that it is not necessarily obvious to the reader that these two are different ways of talking about the same thing, i.e. that one is the negation of the other. > Once considered a property, s, strong(s) and weak(s) are evaluated to > true or false. I think this may mean that only when s, strong(s) and weak(s) are considered as properties is it meaningful to assign a truth value to them. However this interpretation doesn't seem to make much sense because only 's' can be considered as something other than a property_expr, namely a bare sequence_expr. strong(s) and weak(s) must be considered as examples of property_expr. Furthermore I think it is confusing to continue talking about the form s separately because it was explained in the previous section that the form sequence_expr always defaults to one of weak(sequence_expr) or strong(sequence_expr) in different contexts. > The multiplicity of the matches/potential matches beyond whether there > exists one, does not effect the evaluation. This is the sentence I have the hardest to parse and then grasp. First: Could this maybe be rephrased: | The multiplicity of the matches/potential matches beyond the first | one, does not effect the evaluation. Now this is true of strong embedding. However it is not obvious that this is the case for weak embedding: If there is no full match anywhere there needs to be one "potential match" for every cycle of the trace for the property to be evaluated to true. How can this be reconciled with the statement that the "multiplicity of [..]potential matches beyond the first one, does not affect the evaluation"? Best Regards, Johan > Therefore, properties of the form > sequence_expr, (weak(sequence_expr)), and (strong(sequence_expr)) are > evaluated to true if and only if the properties > first_match(sequence_expr), (weak(first_match(sequence_expr))) and > (strong(first_match(sequence_expr))) are evaluated to true > respectively." On Wed, Nov 28, 2007 at 04:01:13PM +0200, Bustan, Doron wrote: > People, what do you think? > > Is my paragraph hard to comprehend? > > Doron > > >>-----Original Message----- > >>From: Johan Martensson [mailto:johan.martensson@jasper-da.com] > >>Sent: Wednesday, November 28, 2007 3:55 PM > >>To: Bustan, Doron > >>Cc: Eduard Cerny; john.havlicek@freescale.com; sv-ac@eda.org > >>Subject: Re: [sv-ac] Re: 1932 LTL.1932.20071114.pdf some errata. > >> > >>Hi Doron, > >> > >>I think the sentence "Once considered a property, s, strong(s) and > >>weak(s) are evaluated to true or false. The multiplicity of the > >>matches/potential matches beyond whether there exists one, does not > >>effect the evaluation." might just exhaust the power of comprehension of > >>the intended audience. > >> > >>I rewrote my suggested replacement to better reflect the informal > >>semantic explanation in the paragraph above this. Also I don't think we > >>need > >>to give a separate explanation for the property sequence_expr since > >>that is defaulting to either strong(sequence_expr) or > >>weak(sequence_expr) as the case may be. > >> > >> > >> > >>REPLACE > >> Since only one match is needed, properties of the form sequence_expr, > >> (weak(sequence_expr)), and (strong(sequence_expr)) are evaluated to > >> true if and only if the properties first_match(sequence_expr), > >> (weak(first_match(sequence_expr))) and > >> (strong(first_match(sequence_expr))) are evaluated to true > >> respectively. As soon as a match of sequence_expr is determined, the > >> evaluation of the property is considered to be true, and no other > >>WITH > >> Since for strong(sequence_expr) only one match is needed, properties of > >> this form are evaluated to true if and only if the corresponding > >> properties of the form (strong(first_match(sequence_expr))) are > >> evaluated to true respectively. As soon as a match of sequence_expr is > >> determined, the evaluation of the property is considered to be true, > >> and no other matches are required for that evaluation attempt. > >> > >> Similarly properties of the form weak(sequence_expr) are evaluated to > >> true if and only if the corresponding properties of the form > >> (weak(first_match(sequence_expr))) are evaluated to true > >> respectively. The reason is that a finite prefix of a trace vitnesses > >> a non-match of a sequence_expr if and only if it vitnesses a non-match > >> of the first_match of that sequence_expr. > >> > >> > >>Best Regards, > >> > >>Johan > >> > >>On Wed, Nov 28, 2007 at 02:03:00PM +0200, Bustan, Doron wrote: > >>> > >>> I wrote the following paragraph, > >>> > >>> "Given a simulation run w, a sequence s may have multiple matches over > >>> prefixes of w. Furthermore, even if there is no prefix of w that > >>> matches s, it could be that every prefix has the potential to match s > >>> in the future in multiple ways. Once considered a property, s, > >>> strong(s) and weak(s) are evaluated to true or false. The multiplicity > >>> of the matches/potential matches beyond whether there exists one, does > >>> not effect the evaluation. Therefore, properties of the form > >>> sequence_expr, (weak(sequence_expr)), and (strong(sequence_expr)) are > >>> evaluated to true if and only if the properties > >>> first_match(sequence_expr), (weak(first_match(sequence_expr))) and > >>> (strong(first_match(sequence_expr))) are evaluated to true > >>> respectively." > >>> > >>> > >>> What do you think? > >>> > >>> Doron > >>> > >>> > >>> >>-----Original Message----- From: owner-sv-ac@server.eda.org > >>> >>[mailto:owner-sv-ac@server.eda.org] On Behalf Of Eduard Cerny Sent: > >>> >>Wednesday, November 21, 2007 3:46 PM To: > >>> >>john.havlicek@freescale.com; Eduard.Cerny@synopsys.com Cc: > >>> >>johan.martensson@jasper-da.com; sv-ac@server.eda.org; Bustan, Doron > >>> >>Subject: Re: [sv-ac] Re: 1932 LTL.1932.20071114.pdf some errata. > >>> >> > >>> >>Yes that makes sense, but the way it was written have the impression > >>> >>that fail of first match is different. > >>> >> > >>> >>Ed > >>> >> > >>> >>Sent from BlackBerry. > >>> >> > >>> >> > >>> >>----- Original Message ----- From: John Havlicek > >>> >><john.havlicek@freescale.com> To: Eduard.Cerny@synopsys.COM > >>> >><Eduard.Cerny@synopsys.COM> Cc: johan.martensson@jasper-da.com > >>> >><johan.martensson@jasper-da.com>; sv- ac@eda.org <sv-ac@eda.org>; > >>> >>doron.bustan@intel.com <doron.bustan@intel.com> Sent: Wed Nov 21 > >>> >>05:16:44 2007 Subject: Re: [sv-ac] Re: 1932 LTL.1932.20071114.pdf > >>> >>some errata. > >>> >> > >>> >>Hi Ed: > >>> >> > >>> >>I interpret this to be saying that if a finite trace has enough > >>> >>information to demonstrate that no match of R is possible, then that > >>> >>same trace has enough information to demonstrate that no match of > >>> >>first_match(R) is possible. > >>> >> > >>> >>J.H. > >>> >> > >>> >> > >>> >>> X-Authentication-Warning: server.eda.org: majordom set sender to > >>> >>> owner- > >>> >>sv-ac@eda.org using -f > >>> >>> X-MimeOLE: Produced By Microsoft Exchange V6.5 Content-class: > >>> >>> urn:content-classes:message Date: Tue, 20 Nov 2007 17:27:03 -0800 > >>> >>> Thread-Topic: [sv-ac] Re: 1932 LTL.1932.20071114.pdf some errata. > >>> >>> thread-index: AcgrkWQ4yR/LEDzMSkW9N23q933ntwASIF4g From: "Eduard > >>> >>> Cerny" <Eduard.Cerny@synopsys.com> X-OriginalArrivalTime: 21 Nov > >>> >>> 2007 01:27:03.0313 (UTC) > >>> >>FILETIME=[9EDD5010:01C82BDD] > >>> >>> X-eda.org-MailScanner: Found to be clean, Found to be clean > >>> >>> X-Spam-Status: No, No X-MIME-Autoconverted: from quoted-printable > >>> >>> to 8bit by server.eda.org id > >>> >>lAL1RJkl001238 > >>> >>> 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 > >>> >>> > >>> >>> Hello Johan, > >>> >>> > >>> >>> You wrote " It is also the case that a finite prefix of a trace > >>> >>contradicts a > >>> >>> sequence_expr if and only if it contradicts the first_match of > >>> >>> that sequence_expr." But what is the difference between > >>> >>> "contradicting the > >>> >>first_match or that sequence expression" and contradicting any > >>> >>match of the sequence_expression"? Since there is no first mathc > >>> >>there is no match at all. > >>> >>> > >>> >>> Thanks, ed > >>> >>> > >>> >>> > >>> >>> > -----Original Message----- From: owner-sv-ac@eda.org > >>> >>> > [mailto:owner-sv-ac@eda.org] On Behalf Of Johan Martensson Sent: > >>> >>> > Tuesday, November 20, 2007 11:20 AM To: sv-ac@eda.org; Bustan, > >>> >>> > Doron Subject: [sv-ac] Re: 1932 LTL.1932.20071114.pdf some > >>> >>> > errata. > >>> >>> > > >>> >>> > Hi Doron, > >>> >>> > > >>> >>> > some problems I found in LTL.1932.20071114.pdf > >>> >>> > > >>> >>> > 16.12. (The paragraph beginning with: "The result of property > >>> >>> > evaluation is either true or false.") ====== > >>> >>> > > >>> >>> > There are lots of problems with this paragraph. > >>> >>> > > >>> >>> > 1) There are now boolean operators for implication and > >>> >>> > equivalence ('implies' and 'iff') which should perhaps be > >>> >>> > mentioned together with negation, disjunction and conjunction. > >>> >>> > 1) I think there should be dots, not hyphen between 'if' and > >>> >>> > 'else'. 2) There should be a comma between 'strong' and > >>> >>> > 'accept_on'. 3) 'and' between 'until' and 'eventually' should > >>> >>> > have different font from that of the operators. 4) > >>> >>> > 'implication' and 'followed_by' are not operators and should > >>> >>> > maybe have different font from that of the operators 'weak', > >>> >>> > 'strong' etc. 5) Maybe the strong variants of next, until, > >>> >>> > always and eventually, and the _with variants of until and > >>> >>> > s_until should also be listed. > >>> >>> > > >>> >>> > 1, 4 and 5 above point to a related set of problems with this > >>> >>> > paragraph: Should we list all the different operators here or > >>> >>> > should we use the grouping provieded by the various following > >>> >>> > subsections 16.12.2-16.12.16. It seems there is no uniform > >>> >>> > principle of reference chosen in this paragraph. > >>> >>> > > >>> >>> > Table 16.25 =========== > >>> >>> > > >>> >>> > The operators 'throughout', 'within', 'intersect', 'and' 'or', > >>> >>> > 'implies' and 'iff' are written with a initial capital letter. > >>> >>> > > >>> >>> > The operators 'implies' and 'iff' are rendered with different > >>> >>> > font from the others.. > >>> >>> > > >>> >>> > 16.12.1 Sequence property ========================= (The > >>> >>> > paragraph beginning with "Since only one match is needed, > >>> >>> > properties ...") > >>> >>> > > >>> >>> > This paragraph is a little strange. The discription seems to > >>> >>> > apply to strong embedding of sequences. For weak embedding not > >>> >>> > even one match of the sequence is required. > >>> >>> > > >>> >>> > If we decide to keep this section maybe it should be split in > >>> >>> > two giving different explanations for the weak and strong case > >>> >>> > respectively. > >>> >>> > > >>> >>> > REPLACE Since only one match is needed, properties of the form > >>> >>> > sequence_expr, (weak(sequence_expr)), and > >>> >>> > (strong(sequence_expr)) are evaluated to true if and only if the > >>> >>> > properties first_match(sequence_expr), > >>> >>> > (weak(first_match(sequence_expr))) and > >>> >>> > (strong(first_match(sequence_expr))) are evaluated to true > >>> >>> > respectively. As soon as a match of sequence_expr is > >>> >>> > determined, the evaluation of the property is considered to be > >>> >>> > true, and no other WITH Since for strong(sequence_expr) only one > >>> >>> > match is needed, properties of this form are evaluated to true > >>> >>> > if and only if the corresponding properties of the form > >>> >>> > (strong(first_match(sequence_expr))) are evaluated to true > >>> >>> > respectively. As soon as a match of sequence_expr is > >>> >>> > determined, the evaluation of the property is considered to be > >>> >>> > true, and no other matches are required for that evaluation > >>> >>> > attempt. > >>> >>> > > >>> >>> > It is also the case that a finite prefix of a trace contradicts > >>> >>> > a sequence_expr if and only if it contradicts the first_match > >>> >>> > of that sequence_expr. Hence properties of the form > >>> >>> > weak(sequence_expr) are evaluated to true if and only if the > >>> >>> > corresponding properties of the form > >>> >>> > (weak(first_match(sequence_expr))) are evaluated to true > >>> >>> > respectively. > >>> >>> > > >>> >>> > 16.12.1-16.12.16 ================ > >>> >>> > > >>> >>> > The headings of these sequences don't seem to be uniformly > >>> >>> > capitalized, for example 16.2.10 has initial capital in "Next > >>> >>> > property" but 16.2.11 has "always property". > >>> >>> > > >>> >>> > These headings seem to serve the purpose of naming different > >>> >>> > operator groups. For example an until property has one of the > >>> >>> > operators until, until_with, s_until or s_until_with as its top > >>> >>> > level operator. Maybe we should define explicit corresponding > >>> >>> > operator groups for use for examples in the section under 16.12 > >>> >>> > discussed above. > >>> >>> > > >>> >>> > This review was only partial, for this time :-(. > >>> >>> > > >>> >>> > Regards, > >>> >>> > > >>> >>> > Johan M > >>> >>> > > >>> >>> > On Wed, Nov 07, 2007 at 11:38:31AM +0100, Johan Martensson > >>> >>> > wrote: > >>> >>> > > Hi Doron, > >>> >>> > > > >>> >>> > > some further errors I found in LTL.1932.20071030.pdf > >>> >>> > > > >>> >>> > > 16.12. (The paragraph beginning with: The result of > >>> >>> > property evaluation > >>> >>> > > is either true or false.) > >>> >>> > > > >>> >>> > > REPLACE (dot after always, should be comma, no comman after > >>> >>> > followed by, > >>> >>> > > and between accept_on and reject_on should not be bold.) > >>> >>> > > > >>> >>> > > The result of property evaluation is either true or false. > >>> >>> > Properties > >>> >>> > > may be built from other properties or sequences using > >>> >>> > > instantiation, boolean operators (negation, disjunction, > >>> >>> > > conjunction, if...else, implication, followed_by weak, strong > >>> >>> > > and iff) and temporal > >>> >>> > operators > >>> >>> > > (next, always. until, eventually, accept_on and reject_on) > >>> >>> > described in > >>> >>> > > the following subclauses. > >>> >>> > > > >>> >>> > > WITH The result of property evaluation is either true or > >>> >>> > > false. > >>> >>> > Properties > >>> >>> > > may be built from other properties or sequences using > >>> >>> > > instantiation, boolean operators (negation, disjunction, > >>> >>> > > conjunction, if...else, implication, followed_by, weak, strong > >>> >>> > > and iff) and > >>> >>> > temporal operators > >>> >>> > > (next, always, until, eventually, accept_on and reject_on) > >>> >>> > described in > >>> >>> > > the following subclauses. > >>> >>> > > > >>> >>> > > > >>> >>> > > > >>> >>> > > 16.12.9 followed_by property > >>> >>> > > > >>> >>> > > REPLACE (I don't think proceed is the right word here) The > >>> >>> > > followed_by construct specifies that the checking of a > >>> >>> > property is > >>> >>> > > required to proceed a match of a sequential antecedent WITH > >>> >>> > > The followed_by construct specifies that the checking of a > >>> >>> > property is > >>> >>> > > required to be preceded by a match of a sequential antecedent > >>> >>> > > > >>> >>> > > REPLACE (followed => followed_by, "at the end point of the > >>> >>> > > match" => "the end point of this match") Two forms of > >>> >>> > > followed_by are provided: overlapped using > >>> >>> > operator #-# and > >>> >>> > > nonoverlapped using operator #=#. For overlapped followed, > >>> >>> > there shall > >>> >>> > > be a match for the antecedent sequence_expr, where at the > >>> >>> > end point of > >>> >>> > > the match is the start point of the evaluation of the > >>> >>> > > consequent property_expr. For nonoverlapped followed_by, the > >>> >>> > > start point of the evaluation of the consequent property_expr > >>> >>> > > is the clock > >>> >>> > tick after the > >>> >>> > > end point of the match. WITH Two forms of followed_by are > >>> >>> > > provided: overlapped using > >>> >>> > operator #-# and > >>> >>> > > nonoverlapped using operator #=#. For overlapped > >>> >>> > followed_by, there shall > >>> >>> > > be a match for the antecedent sequence_expr, where the end > >>> >>> > > point of this match is the start point of the evaluation of > >>> >>> > > the consequent property_expr. For nonoverlapped followed_by, > >>> >>> > > the start point of the evaluation of the consequent > >>> >>> > > property_expr is the clock > >>> >>> > tick after the > >>> >>> > > end point of the match. > >>> >>> > > > >>> >>> > > REPLACE (remove ##1 in two places) The followed_by operators > >>> >>> > > are the duals of the implication > >>> >>> > operators. > >>> >>> > > Therefore, sequence_expr #-# property_expr is equivalent to > >>> >>> > the following: > >>> >>> > > > >>> >>> > > not sequence_expr ##1 1 |-> not property_expr > >>> >>> > > > >>> >>> > > and sequence_expr #=# property_expr is equivalent to the > >>> >>> > > following: > >>> >>> > > > >>> >>> > > not sequence_expr ##1 1 |=> not property_expr WITH The > >>> >>> > > followed_by operators are the duals of the implication > >>> >>> > operators. > >>> >>> > > Therefore, sequence_expr #-# property_expr is equivalent to > >>> >>> > the following: > >>> >>> > > > >>> >>> > > not sequence_expr |-> not property_expr > >>> >>> > > > >>> >>> > > and sequence_expr #=# property_expr is equivalent to the > >>> >>> > > following: > >>> >>> > > > >>> >>> > > not sequence_expr |=> not property_expr > >>> >>> > > > >>> >>> > > 16.12.10 > >>> >>> > > > >>> >>> > > REPLACE (expression => const_expression, constants => > >>> >>> > const_expression, > >>> >>> > > constant_expression => const_expression) Weak next property > >>> >>> > > evaluates to true if property_expr holds > >>> >>> > at the next > >>> >>> > > clock tick or if there are no further clock ticks. To > >>> >>> > require the clock > >>> >>> > > tick to occur, use the strong form s_next property_expr. Weak > >>> >>> > > next property with expression evaluates to true if > >>> >>> > > property_expr > >>> >>> > holds in the > >>> >>> > > specified of future clock ticks indicated by the constants, > >>> >>> > or if there > >>> >>> > > are not enough clock ticks for the property to complete the > >>> >>> > evaluation. > >>> >>> > > To require the necessary clock ticks to occur use the > >>> >>> > strong form s_next > >>> >>> > > [constant_expression] property_expr. WITH Weak next property > >>> >>> > > evaluates to true if property_expr holds > >>> >>> > at the next > >>> >>> > > clock tick or if there are no further clock ticks. To > >>> >>> > require the clock > >>> >>> > > tick to occur, use the strong form s_next property_expr. Weak > >>> >>> > > next property with const_expression evaluates to true if > >>> >>> > property_expr holds in the > >>> >>> > > specified of future clock ticks indicated by the > >>> >>> > const_expression, or if there > >>> >>> > > are not enough clock ticks for the property to complete the > >>> >>> > evaluation. > >>> >>> > > To require the necessary clock ticks to occur use the > >>> >>> > strong form s_next > >>> >>> > > [const_expression] property_expr. > >>> >>> > > > >>> >>> > > I just read to this poin this time. Hopefully I get some > >>> >>> > time to read > >>> >>> > > the rest. > >>> >>> > > > >>> >>> > > Best Regards, > >>> >>> > > > >>> >>> > > Johan > >>> >>> > > > >>> >>> > > > >>> >>> > > -- > >>> >>> > > ------------------------------------------------------------ > >>> >>> > > Johan Mårtensson Office: +46 31 7451913 Jasper > >>> >>> > > Design Automation Mobile: +46 703749681 Arvid Hedvalls > >>> >>> > > backe 4 Fax: +46 31 7451939 411 33 Gothenburg, > >>> >>> > > Sweden Skype ID: johanmartensson > >>> >>> > > ------------------------------------------------------------ > >>> >>> > > >>> >>> > -- ------------------------------------------------------------ > >>> >>> > Johan Mårtensson Office: +46 31 7451913 Jasper > >>> >>> > Design Automation Mobile: +46 703749681 Arvid Hedvalls > >>> >>> > backe 4 Fax: +46 31 7451939 411 33 Gothenburg, Sweden > >>> >>> > Skype ID: johanmartensson > >>> >>> > ------------------------------------------------------------ > >>> >>> > > >>> >>> > > >>> >>> > -- This message has been scanned for viruses and dangerous > >>> >>> > content by MailScanner, and is believed to be clean. > >>> >>> > > >>> >>> > > >>> >>> > >>> >>> -- This message has been scanned for viruses and dangerous content > >>> >>> by MailScanner, and is believed to be clean. > >>> >>> > >>> >>> > >>> >> > >>> >>-- This message has been scanned for viruses anddangerous content by > >>> >>MailScanner, and isbelieved 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 > >>Arvid Hedvalls backe 4 Fax: +46 31 7451939 > >>411 33 Gothenburg, Sweden Skype ID: johanmartensson > >>------------------------------------------------------------ > --------------------------------------------------------------------- > 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 Arvid Hedvalls backe 4 Fax: +46 31 7451939 411 33 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 Nov 29 01:29:02 2007
This archive was generated by hypermail 2.1.8 : Thu Nov 29 2007 - 01:29:11 PST