RE: Group A - first draft LRM changes

One last addition on this topic:

On re-reading the formal semantic definition for abort in Dana's 1/26/03 email:

| 5. Definition of clocked semantics for f abort b : replaced
| w^i|= c/\ b by w^i |=(T) c /\ b
| (that is added context \true to the |= symbols)

I realized that in fact this definition STILL has the abort condition sensitive to the clock. However, in a later draft of Appendix B, dated July 4, 2003, the reference to the clock is gone from the abort semantics. So it appeared that the change occurred during the development of PSL v1.1, in the Alignment subcommittee.

The first place in which the clock reference disappeared from the abort semantics seems to be the draft paper entitled "A preliminary proposal for Sugar2.0 semantics - "Truncated/Untruncated Semantics", dated Dec 9, 2002. That paper proposed a strong/weak/neutral semantics for LTL plus abort, on finite and infinite paths. The semantics of abort in PSL v1.1 were ultimately defined to follow what was given in that paper, which was

  w |= f abort_T b <==> either w satisfies f [i.e. f holds neutrally on w] or
    there exists k such that w^k satisfies Boolean b and for every j<k,
      w^j does not satisfy Boolean b and w^(0..k-1) weakly satisfies f.

Note that this paper did not address clocked semantics at all - the entire discussion of LTL was given in terms of unclocked semantics. The focus here was not on clocked vs. unclocked, but rather on strong/weak/neutral semantics.

This suggests that the change to a fixed asynchronous abort in PSL v1.1 (from the abort that was affected by the clock context in PSL v1.01) might have occurred accidentally, as a result of applying the new definition of abort without first extending it to consider clocking. It is also possible that the new abort semantics were left unaffected by the clock context due to the influence of the SVA 'disable iff' clause, which is only used to model asynchronous reset.

If there was a conscious decision not to extend the new abort definition to consider clocking, I can't find any documentation of that decision. I recall thinking at the time that PSL abort semantics included those of SVA 'disable iff', but were not limited to those semantics, because (I thought) PSL aborts could also be clocked.

I can find no subsequent acknowledgement that the semantics of abort changed in PSL v1.1 w.r.t. the effect of the clock context on the abort operator. In particular, the Final Report of the Alignment Subcommittee (see http://www.eda.org/vfv/hm/1216.html) mentions the adoption of new abort semantics, but does not appear to mention any change with regard to clocking of abort.

Regards,

Erich

| -----Original Message-----
| From: owner-ieee-1850-extensions@eda.org
| [mailto:owner-ieee-1850-extensions@eda.org] On Behalf Of
| Erich Marschner
| Sent: Thursday, December 16, 2004 12:34 PM
| To: Cindy Eisner
| Cc: Johan Mårtensson; ieee-1850-extensions@eda.org;
| bassam@novas.com; dana.fisman@weizmann.ac.il
| Subject: RE: Group A - first draft LRM changes
|
|
| Hi Cindy,
|
| Ii apologize for dragging this out further, but I'd really
| like to understand when and why the decision was made to make
| abort asynchronous.
|
| I've just gone back and looked at the requirements, and I see
| no requirement for an asynchronous abort.
|
| The first set of requirements were captured in a spreadsheet
| that is still visible by following the "Requirements" link
| from the FVTC web page (http://www.eda.org/vfv), or by going
| directly to
|
| http://www.eda.org/vfv/requirements.htm.
|
| Note requirement 33, which says "Allow Asynchronous
| modeling/properties". I believe this is the only reference
| to asynchronous behavior in that list.
|
| The second, more detailed set of possible requirements was
| captured in a PDF document that was drafted in late 2001.
| The individual requirements were balloted in October 2001,
| and the results were reported by Harry in an email entitled
| "VFV Committee Final Requirements", dated Sunday Nov 4 2001,
| which can be found in the FVTC mail archive at
|
| http://www.eda.org/vfv/hm/0440.html.
|
| I cannot locate any occurrence of 'asynchronous' (or
| 'asynch') in this set of requirements.
|
| I also scanned my local copies of FVTC email for 'asynch',
| from November 2001 to November 2003. I found no discussion
| of making abort asynchronous.
|
| I did find the following text in an early draft of the LRM
| section on Property Declaration (8/25/02, written by me):
|
| This property could also be declared as follows:
|
| property ResultAfterN (boolean start, stop; property
| result; const n) =
| always ((start -> next[n] (result)) @ (posedge clk)
| abort stop);
|
| The two declarations have slightly different interfaces
| (i.e., different formal
| parameter orders), but they both declare the same
| property ResultAfterN. This
| property describes behavior in which a specified result (a
| property) occurs N
| cycles after an enabling condition (parameter 'start')
| occurs, with cycles defined
| by rising edges of signal 'clk', unless an (asynchronous)
| abort condition
| (parameter 'stop') occurs.
|
| This example and its explanation suggest that at the time,
| I/we understood that putting the 'abort' condition outside
| the scope of the clock expression would make the abort
| asynchronous. (By the way, this text is still in the PSL
| v1.1 LRM, on page 82, including the "(asynchronous)" qualifier.)
|
| I finally found a reference to a change in the semantics of
| abort in my archive of email related to drafting the initial
| LRM. An email from Dana (dated 1/26/03) appears to represent
| the point at which the change occurred. Here is the main
| text of that message:
|
| Attached is the latest formal semantics document (dated
| January 23), reflecting
| the corrections of the typos pointed out by Mike.
|
| The changes compared to the December 10 version are:
|
| 1. Rewrite rule for r@c: changed r1 to r and added curly brackets
| around "c1:\T^c1{r}"
| 2. Definition of clocked semantics for Boolean: replaced w by
| \ell^0
| 3. Definition of clocked semantics for r@c1: replaced
| w^{0,i}|={!c1[*];c1} by w^{0,i}|=(T) {!c1[*];c1}
| (that is added context \true to the |= symbols)
| 4. Definition of clocked semantics for f@c1: replaced
| w^{0,i}|={!c1[*];c1} by w^{0,i}|=(T) {!c1[*];c1}
| (that is added context \true to the |= symbols)
| 5. Definition of clocked semantics for f abort b : replaced
| w^i|= c/\ b by w^i |=(T) c /\ b
| (that is added context \true to the |= symbols)
|
| The motto of changes 3-5 is that clocked semantics relies
| only on clocked semantics
| and Boolean unlocked semantics and does not rely on
| unclocked semantics for SEREs or
| formulas. Thus whenever we used |= with out a context in
| the unclocked semantics, I
| changed it to |=(T) if the left hand side of |= is a word
| and left it with no context
| if the left hand side is a letter.
|
| Item 5 above shows that the original semantics (in which the
| abort condition was sensitive to the clock) were changed so
| that the abort condition would no longer be sensitive to the
| clock. The subsequent paragraph seems to say that the change
| was made to be consistent with a general pattern of semantic
| definition, NOT that it was done specifically to support
| modeling of asynchronous reset.
|
| I should note that there was also the issue about the
| definition of abort that Moshe Vardi raised. This is
| mentioned in an email from Cindy on 11/26/02:
|
| 2. as pointed out by moshe vardi et al in
| www.cs.rice.edu/~vardi/misc/abortreset.pdf,
| the complexity of the abort operator is problematical. we
| plan on addressing this issue
| by modifying the semantics of abort to what vardi et all
| term "reset semantics". thus, in
| the semantics presented above the formula ((eventually!
| false) abort b) must fail in all
| designs, while in version 1.1, we plan on allowing this
| formula to pass in if 'b' is
| asserted. from the user's point of view, this will have
| minimal effect, since it is a
| corner case resulting from aborting a non-satisfiable
| formula. from a tool builder's
| point of view, this will have minimal effect since the
| change involves removing one step
| in the algorithm that builds the automaton for a given
| formula (the step that removes
| states from which there is no accepting run).
|
| I am not aware that this issue dictated an asynchronous abort
| instead of an abort that could be sensitive to the clock
| context, although I suppose there might be a connection.
|
| So for what it's worth, that's what I can find in the
| historical record. I clearly missed the change of abort
| semantics in January 2003, and I've misunderstood them since
| then. At this point, I still think that that change was
| unnecessary and inappropriate, because it breaks the general
| pattern of how we specify whether a property is synchronous
| (or not) by applying a clock expression (or not).
|
| Regards,
|
| Erich
|
|
| | -----Original Message-----
| | From: Cindy Eisner [mailto:EISNER@il.ibm.com]
| | Sent: Thursday, December 16, 2004 4:18 AM
| | To: Erich Marschner
| | Cc: Johan Mårtensson; ieee-1850-extensions@eda.org;
| bassam@novas.com;
| | dana.fisman@weizmann.ac.il
| | Subject: RE: Group A - first draft LRM changes
| |
| |
| |
| |
| |
| | erich, johan, all,
| |
| | if i recall correctly, the decision to make abort
| asynchronous was one
| | of the requirements drawn up by the committee. the idea,
| as johan has
| | pointed out, is that you can always make the abort synchronous by
| | "anding" the abort condition with the clock, but to do the
| opposite is
| | difficult.
| |
| | if we are going to make a change, i would suggest replacing "abort"
| | with "abort_async" and "abort_sync", which are respectively, an
| | asynchronous abort and a synchronous one.
| |
| | cindy.
| |
| | --------------------------------------------------------------------
| | Cindy Eisner
| | Formal Methods Group
| | IBM Haifa Research Laboratory
| | Haifa 31905, Israel
| | Tel: +972-4-8296-266
| | Fax: +972-4-8296-114
| | e-mail: eisner@il.ibm.com
| |
| | "Erich Marschner" <erichm@cadence.com>@eda.org on
| 16/12/2004 00:09:53
| |
| | Sent by: owner-ieee-1850-extensions@eda.org
| |
| |
| | To: Johan Mårtensson <johan.martensson@safelogic.se>,
| | <ieee-1850-extensions@eda.org>
| | cc: <bassam@novas.com>, Cindy Eisner/Haifa/IBM@IBMIL,
| | <dana.fisman@weizmann.ac.il>
| | Subject: RE: Group A - first draft LRM changes
| |
| |
| | Johan,
| |
| | | This is certainly possible but if you wanted to express
| | asynchronous
| | | abort you would sometimes have to use fairly twisted syntax
| | given this
| | | "synchronous" definition.
| |
| | We have two choices. We can
| |
| | 1. make language forms sensitive to the clock context by
| default, and
| | apply some transformation to shield them from it when we don't want
| | the default behavior; or
| |
| | 2. make language forms insensitive to the clock context by default,
| | and apply some transformation to make them sensitive to it when we
| | don't want the default behavior.
| |
| | The first approach is what we do for sequences and for nearly all
| | properties - they are sensitive to the clock context,
| unless we shield
| | them from that context by clocking them with @True.
| |
| | The second approach is what apparently applies now to the abort
| | condition.
| | Unfortunately the transformation you have suggested ('and'ing the
| | clock expression with the abort condition) doesn't work as
| well when
| | the clock expression is something like @(posedge clk),
| which is not a
| | Boolean and therefore cannot be 'and'ed with anything; in
| such a case
| | the clock expression must be transformed itself into something else
| | (e.g., rose(clk)) before you can do this - so for example,
| you might
| | end up writing
| |
| | always (a -> b)@(posedge clk) abort (c && rose(clk));
| |
| | This one turns out to be relatively simple, but what would
| you do if
| | the clock expression above were @(x,y,z) instead of
| @(posedge clk)? I
| | supposed you could write
| |
| | always (a -> b)@(x,y,z) abort (c && (rose(x) || fell(x)
| | || rose(y) ||
| | fell(y) || ...);
| |
| | but I don't think this is very readable.
| |
| | Of the two approaches, I view the second one as more 'twisted' than
| | the first - and the fact that we are requiring users to
| understand and
| | apply BOTH approaches is even worse.
| | I would prefer to ask the user to understand and apply only
| the first
| | approach.
| |
| |
| | | > but by that argument we don't need clock expressions at
| | all: every
| | | > condition could be 'and'ed with the clock.
| | |
| | | This is not true, if I understand you correctly. Just to take the
| | | simplest (of many possible) example.
| | |
| | | The formula a@c is not equivalent to a&c.
| |
| | Yes, you are right. I would say this is another reason for
| sticking
| | to the one, simple mechanism of applying a clock context via the @
| | operator, rather than encouraging users to 'and' a clock condition
| | with a Boolean under certain circumstances (but not others).
| |
| | Regards,
| |
| | Erich
| |
| |
| | | -----Original Message-----
| | | From: Johan Mårtensson [mailto:johan.martensson@safelogic.se]
| | | Sent: Wednesday, December 15, 2004 3:22 PM
| | | To: ieee-1850-extensions@eda.org; Erich Marschner
| | | Cc: bassam@novas.com; Cindy Eisner; dana.fisman@weizmann.ac.il
| | | Subject: Re: Group A - first draft LRM changes
| | |
| | | Erich,
| | |
| | | I think you could achieve what you want not by clocking
| the boolean
| | | semantic relation; It doesn't seem to make sense because
| | this relation
| | | relates single letters and booleans.
| | | Instead you could certainly change the abort case of the
| definition
| | | to.
| | |
| | | v|=(c) phi abort b <==> either v|=(c) phi or there exists
| | j<|v| s.t.
| | | v^j |= b&c and v^(0..j-1)T^(omega) |=(c) phi
| | |
| | | This is certainly possible but if you wanted to express
| | asynchronous
| | | abort you would sometimes have to use fairly twisted syntax
| | given this
| | | "synchronous" definition.
| | |
| | | I have a comment on what you write below.
| | |
| | | On Wed, Dec 15, 2004 at 11:22:21AM -0800, Erich Marschner wrote:
| | |
| | |
| | | > Bassam,
| | | >
| | | > While I am admittedly myopic, I don't see a problem with
| | | extending the
| | | > formal definition to support synchronous abort. The current
| | | > definition (in B.3.1.2.2, Semantics of clocked FL) is:
| | | >
| | | > v|=(c) phi abort b <==> either v|=(c) phi or there exists
| | | j<|v| s.t.
| | | > v^j |= b and v^(0..j-1)T^(omega) |=(c) phi
| | | >
| | | > I would think that we would only need to change
| | | >
| | | > v^j |= b
| | | >
| | | > to
| | | >
| | | > v^j |=(c) b
| | | >
| | | > to make the abort sensitive to the clock context. (Whether
| | | this might
| | | > create other issues within the formal semantics, I don't know.)
| | | >
| | | > Yes, you can get the same effect by 'tweaking' the abort
| | | condition -
| | | > e.g.,
| | | >
| | | > always (a -> b)@clk abort (c&&clk);
| | | >
| | | > but by that argument we don't need clock expressions at
| | all: every
| | | > condition could be 'and'ed with the clock.
| | |
| | | This is not true, if I understand you correctly. Just to take the
| | | simplest (of many possible) example.
| | |
| | | The formula a@c is not equivalent to a&c.
| | |
| | | The first but not the second is true in the following situation
| | |
| | | a:001000
| | | c:001000
| | |
| | | Best Regards, Johan M
| | |
| | | > The point of having a clock
| | | > expression is to factor out the clock and make it easy to
| | specify a
| | | > synchronous property, so it is strange not to apply it
| | consistently.
| | | >
| | | > I agree that if support for synchronous reset is important
| | | enough for
| | | > PSL to adopt, then it is also important enough for SVA to
| | | adopt. The
| | | > fact that you have already raised the same issue in the SVA
| | | committee
| | | > suggests that there is some reason to support this in both
| | | languages.
| | | >
| | | > Regards,
| | | >
| | | > Erich
| | | >
| | | >
| | | > | -----Original Message-----
| | | > | From: Bassam Tabbara [mailto:bassam@novas.com]
| | | > | Sent: Wednesday, December 15, 2004 1:25 PM
| | | > | To: Erich Marschner; 'Johan Mårtensson'; 'Cindy Eisner';
| | | > | dana.fisman@weizmann.ac.il
| | | > | Cc: ieee-1850-extensions@eda.org
| | | > | Subject: RE: Group A - first draft LRM changes
| | | > |
| | | > | Erich,
| | | > |
| | | > | First off I agree with you about practicality, and the
| | | fact that the
| | | > | informal LRM description can be reasonably and easily
| | | overloaded to
| | | > | mean this (but not formal defs). I wanted to note 2
| things here:
| | | > |
| | | > | 1) We also had a similar discussion in the context of SVA
| | | recently
| | | > | where I suggested this same "natural fix" to disable
| iff (but no
| | | > | sale) and John pointed out the formal semantics of SVA
| | | and alignment
| | | > | to PSL's semantics (which Johan cites).
| | | > | 2) Other users on SVA committee also pointed out that an
| | | > | "asynchronous" is general enough, so by tweaking the
| | | abort condition
| | | > | to be synchronous you can get the synchronous overall
| | | effect, albeit
| | | > | it's not as easy/practical as the suggestion you make below.
| | | > |
| | | > | I'm not sure if "alignment" considerations are of utmost
| | | importance
| | | > | here necessarily, just a point of reference as it were if
| | | it indeed
| | | > | is something to keep in mind. It works both
| | | > | ways: If the change is deemed worthwhile in PSL, SVA
| | | should consider
| | | > | this issue again in the future.
| | | > |
| | | > | Thx.
| | | > | -Bassam.
| | | > |
| | | > | --
| | | > | Dr. Bassam Tabbara
| | | > | Architect, R&D
| | | > | Novas Software, Inc.
| | | > | (408) 467-7893
| | | > |
| | | > | -----Original Message-----
| | | > | From: owner-ieee-1850-extensions@eda.org
| | | > | [mailto:owner-ieee-1850-extensions@eda.org] On Behalf
| Of Erich
| | | > | Marschner
| | | > | Sent: Wednesday, December 15, 2004 8:37 AM
| | | > | To: Johan Mårtensson; Cindy Eisner; dana.fisman@weizmann.ac.il
| | | > | Cc: ieee-1850-extensions@eda.org
| | | > | Subject: RE: Group A - first draft LRM changes
| | | > |
| | | > | Johan,
| | | > |
| | | > | Again, I'm not sure I follow your example (did you mean
| | a abort b
| | | > | instead of b abort a?), but in any case I see now
| that both the
| | | > | clock rewrite rules and the formal semantic definition in
| | | B.3.1.2.2
| | | > | reflect your statement that the abort condition is not
| | | affected by
| | | > | the clock context.
| | | > |
| | | > | I believe this is a problem, from a practical point of view.
| | | > | The abort clause is the natural way to represent
| interrupts and
| | | > | reset operations, and these can be both synchronous or
| | | asynchronous.
| | | > | PSL should allow the user to control whether the abort
| | condition
| | | > | represents a synchronous or an asynchronous event, and
| | | the way to do
| | | > | that is to allow the user to clock it or not, as
| | | appropriate. Thus
| | | > | if I write
| | | > |
| | | > | always (a -> b abort c)@clk
| | | > |
| | | > | I would expect the abort condition to be synchronous;
| | | whereas if I
| | | > | write
| | | > |
| | | > | always (a -> b)@clk abort c
| | | > |
| | | > | I would expect the abort condition to be asynchronous.
| | | > |
| | | > | I see that there may be some issues with nested aborts,
| | | or equally
| | | > | with top-level aborts in the context of a default clock
| | | declaration,
| | | > | because (if abort were defined such that it is affected
| | | by the clock
| | | > | context) it seems difficult to protect the abort
| | | condition from the
| | | > | influence of an outer clock (e.g., to define an
| | | asynchronous abort
| | | > | within a synchronous context) without changing the abort
| | | condition
| | | > | to a property, which is not allowed.
| | | > | For example, assuming that abort is affected by the clock
| | | context,
| | | > | then
| | | > |
| | | > | default clock = clk2
| | | > |
| | | > | always (a -> b)@clk abort c -- abort would be
| | | > | synchronous w.r.t.
| | | > | clk2
| | | > | always (a -> b)@clk abort c@True -- illegal because
| | | > | abort requires a
| | | > | Boolean
| | | > |
| | | > | But we could still write
| | | > |
| | | > | always ((a -> b)@clk abort c)@True -- True hides clk2
| | | > | for the entire
| | | > | property
| | | > |
| | | > | so this shouldn't be an issue.
| | | > |
| | | > | It would seem to be straightforward to define abort in
| | such a way
| | | > | that the clock context applies to the abort condition as
| | | well as to
| | | > | the property.
| | | > | Cindy, Dana, can either of you comment on why this
| wasn't done?
| | | > |
| | | > | Regards,
| | | > |
| | | > | Erich
| | | > |
| | | > |
| | | > |
| | | > |
| | | > | | -----Original Message-----
| | | > | | From: Johan Mårtensson
| [mailto:johan.martensson@safelogic.se]
| | | > | | Sent: Wednesday, December 15, 2004 10:51 AM
| | | > | | To: ieee-1850-extensions@eda.org; Erich Marschner
| | | > | | Subject: Re: Group A - first draft LRM changes
| | | > | |
| | | > | | Erich,
| | | > | |
| | | > | | in fact nested aborts are asyncronous with resepect to
| | | the clock
| | | > | | in the environment. The simplest way to see this is in the
| | | > | case for abort
| | | > | | in the clock rewriting rules (B.5):
| | | > | |
| | | > | | F^c(phi abort b) ==> F^c(phi) abort b
| | | > | |
| | | > | | which means that the abort condition b is left entirely
| | | > | untouched by
| | | > | | the clock rewriting and will thus abort on the first
| | | > | occurrence of b,
| | | > | | whether or not it occurs on a clock instance.
| | | > | |
| | | > | | We can also go through a simple example using the formal
| | | > | semantics for
| | | > | | clocked FL (B.3.1.2.2) directly
| | | > | |
| | | > | | Let v be a word with the following truth values for
| a, b and c
| | | > | |
| | | > | | t: 0123456....
| | | > | | a: 0100000....
| | | > | | b: 0000000....
| | | > | | c: 0010010....
| | | > | |
| | | > | | let v|c be the word containing only those letters of v
| | | > | where c is true
| | | > | |
| | | > | | t: 25....
| | | > | | a: 00....
| | | > | | b: 00....
| | | > | | c: 11....
| | | > | |
| | | > | |
| | | > | | I will use the following symbolism (a_1,...a_n) is a letter
| | | > | | (state) in which signals a_1,..,a_n and no others are
| | true and
| | | > | | <l_0,l_1,....> is a word defined by letters l_1,l_2,...
| | | > | |
| | | > | | Thus v above can be defined as <(),(a),(c),(),(),...>
| | | if a, b and
| | | > | | c are the only signals, and v|c as <(c),(c),(c),...>
| | | > | |
| | | > | | It is easy to see using the definition in B.3.1.2.2 that
| | | > | |
| | | > | | v|= (b abort a)@c
| | | > | |
| | | > | | but
| | | > | |
| | | > | | not v|c |= b abort a
| | | > | |
| | | > | | Best Regards, Johan M
| | | > | |
| | | > | |
| | | > | |
| | | > | | On Wed, Dec 15, 2004 at 07:22:49AM -0800, Erich
| | Marschner wrote:
| | | > | | > Johan,
| | | > | | >
| | | > | | > I don't follow this part of your comment:
| | | > | | >
| | | > | | > | ((always a) abort b)@c is true in the following
| situation
| | | > | | (because
| | | > | | > | it is equivalent to (always a)@c abort b.)
| | | > | | >
| | | > | | > I would think that the @c would apply to "abort b" as well
| | | > | | as to (always a), so I wouldn't expect ((always a)
| | | abort b)@c to
| | | > | | be equivalent to ((always a)@c abort b).
| | | > | | >
| | | > | | > Can you explain why this equivalence should hold?
| | | > | | >
| | | > | | > Regards,
| | | > | | >
| | | > | | > Erich
| | | > | | >
| | | > | | >
| | | > | | > | -----Original Message-----
| | | > | | > | From: Johan Mårtensson
| | | [mailto:johan.martensson@safelogic.se]
| | | > | | > | Sent: Wednesday, December 15, 2004 9:33 AM
| | | > | | > | To: ieee-1850-extensions@eda.org; Erich Marschner
| | | > | | > | Subject: Re: Group A - first draft LRM changes
| | | > | | > |
| | | > | | > | Hi Erich,
| | | > | | > |
| | | > | | > | I have a comment below on your
| | | > | | > |
| | | > | | > | > 4. Correct the informal semantics of '@' to
| allow for a
| | | > | | > | nested subelement that has a different clock context.
| | | > | | > | >
| | | > | | > | > - in Clause 6.1.2.5, Clocked SERE, change the informal
| | | > | | > | semantics to read
| | | > | | > | > as follows: "For unclocked SERE A and Boolean
| | CLK: A@CLK
| | | > | | > | holds tightly
| | | > | | > | > on a given path iff CLK holds in the last
| cycle of the
| | | > | | > | given path, and
| | | > | | > | > A holds tightly on the path obtained by
| extracting the
| | | > | | > | from the given
| | | > | | > | > path exactly those cycles in which CLK
| holds, and any
| | | > | | subordinate
| | | > | | > | > sequences of A hold tightly as specified by A on the
| | | > | | corresponding
| | | > | | > | > sub-paths of the given path."
| | | > | | > | >
| | | > | | > | > - in clause 6.2.1.2, Clocked FL properties, change
| | | > | the informal
| | | > | | > | > semantics to read as follows: "For unclocked
| | FL property
| | | > | | > | A and Boolean
| | | > | | > | > CLK: A@CLK holds on a given path iff A holds
| | on the path
| | | > | | > | obtained by
| | | > | | > | > extracting from the given path exactly those cycles
| | | > | | in which CLK
| | | > | | > | > holds, and any subordinate properties of A hold as
| | | > | | > | specified by A at
| | | > | | > | > the corresponding cycles of the given path."
| | | > | | > | >
| | | > | | > | > [Note: I'm not happy with this yet, but this is the
| | | > | | best I've been
| | | > | | > | > able to do so far.]
| | | > | | > | >
| | | > | | > |
| | | > | | > | Note that there is not only a problem with
| nested clocked
| | | > | | > | subproperties here. Also nested aborts break the clock
| | | > | projection
| | | > | | > | hypothesis. For instance the property
| | | > | | > |
| | | > | | > | ((always a) abort b)@c is true in the following
| situation
| | | > | | (because
| | | > | | > | it is equivalent to (always a)@c abort b.)
| | | > | | > |
| | | > | | > | c:0101010...
| | | > | | > | a:0100000...
| | | > | | > | b:0010000...
| | | > | | > |
| | | > | | > | whereas
| | | > | | > |
| | | > | | > | ((always a) abort b) is not true in
| | | > | | > |
| | | > | | > | a:100...
| | | > | | > | b:000...
| | | > | | > |
| | | > | | > | which is the path obtained when extracting from
| the given
| | | > | | path those
| | | > | | > | cycles in which c holds.
| | | > | | > |
| | | > | | > | It seems this problem with abort and clock projection is
| | | > | | not noted
| | | > | | > | in the current informal semantics in 6.2.1.2 either.
| | | > | | > |
| | | > | | > | Best Regards, Johan M.
| | | > | | > |
| | | > | | > | --
| | | > | | > |
| | ------------------------------------------------------------
| | | > | | > | Johan Martensson, PhD Office: +46 31 7451913
| |
| | | > | | > | R&D Mobile: +46 703749681
| | | > | | > | Safelogic AB Fax: +46 31 7451939
| | | > | | > | Arvid Hedvalls Backe 4
| | | johan.martensson@safelogic.se
| | | > | | > | SE-411 33 Gothenburg, SWEDEN PGP key ID A8857A60
| | | > | | > | www.safelogic.se
| | | > | | > |
| | ------------------------------------------------------------
| | | > | | > |
| | | > | | > |
| | | > | | > |
| | | > | |
| | | > | | --
| | | > | | ------------------------------------------------------------
| | | > | | Johan Martensson, PhD Office: +46 31 7451913
| |
| | | > | | R&D Mobile: +46 703749681
| | | > | | Safelogic AB Fax: +46 31 7451939
| | | > | | Arvid Hedvalls Backe 4
| johan.martensson@safelogic.se
| | | > | | SE-411 33 Gothenburg, SWEDEN
| | | > | | PGP key ID A8857A60
| | | > | | www.safelogic.se
| | | > | | ------------------------------------------------------------
| | | > | |
| | | > | |
| | | > | |
| | | > |
| | | > |
| | | > |
| | | > |
| | | > |
| | |
| | | --
| | | ------------------------------------------------------------
| | | Johan Martensson, PhD Office: +46 31 7451913
| | | R&D Mobile: +46 703749681
| | | Safelogic AB Fax: +46 31 7451939
| | | Arvid Hedvalls Backe 4 johan.martensson@safelogic.se
| | | SE-411 33 Gothenburg, SWEDEN
| | | PGP key ID A8857A60
| | | www.safelogic.se
| | | ------------------------------------------------------------
| | |
| | |
| | |
| |
| |
| |
| |
| |
|
|
|
Received on Thu Dec 16 11:32:55 2004