Re: Group A - first draft LRM changes

Erich,

as I said I see no problem with introducing an exclusively synchronous
abort operator if there is indeed a demand for that. Call it synch_abort
or abort_synch or whatever you like. What you seem to propose however is
that we change the semantics of the current abort operator from
asynchronous to synchronous. This would be a major undertaking:

1) Firstly there is the backwards compatibility issue. There are lots of
properties out there which would have to be rewritten to work as
expected!

2) Secondly I think the question of how complicated it would be to
express asyncronous abort with the synchronous semantics needs to be
investigated more thouroghly.

3) Thirdly there is the SVA alignment issue.

I still think an investigation of 2 would show that expressing
asynchronous abort using a synchronous abort operator will be
complicated and awkward even for fairly natural examples.

Anyway, in light of 1,2,3 such a change doesn't sound like something for
the current iteration.

However, introduction of a abort_synch operator with synchronous
semantics doesn't bring up either of problems 1, 2 or 3, so such a
change would carry much less cost. Still we need to ask ourselves
whether this is what we should put our scant first iteration resourses
on.

An aside: I am very surprised, to say the least, that such a fundamental
semantic issue should be questioned in this forum at this stage. I was
not present when the current semantics of the abort operator was
decided, but surely the pros and cons of asyncronous reset must have
been discussed thourughly at that point.

Best Regards, Johan M

On Thu, Dec 16, 2004 at 07:14:03AM -0800, Erich Marschner wrote:
> Johan,
>
> In my experience so far with users, the 'abort' operator has been used to express various ideas, not all of which are asynchronous reset. Many synthesizable designs involve synchronous reset, NOT asynchronous reset. Also, 'abort' can be used to model other things, such as interrupts, which are typically synchronous. So I believe it is inappropriate to view 'abort' as being solely for asynchronous reset.
>
> I completely agree that you need to be able to model both synchronous and asynchronous abort. But we already have a mechanism in the language that supports this - the use (or non-use) of a clock expression, which is a very natural way of stating that some property, or part thereof, is synchronous (or not). And we have a standard means of hiding an inner, asynchronous property from the influence of an outer clock context - @True. Everywhere else in the language we use these mechanisms without labeling them as 'twisted'. Why can we not apply the same mechanisms to the abort operator?
>
> | If we instead change the definition of abort as you suggest
> | then -- apart from nasty backwards compatibility issues which
> | should not be taken lightly -- users that would like to use
> | abort for handling resets in the way described above would
> | have to write 'twisted' things like.
> |
> | (always r|=>(f@c abort b)@TRUE)@c
> |
> | for what is currently expressed by
> |
> | (always r|=>f abort b)@c
>
> Your asynchronous abort alternative is more complicated than I would make it. Assuming that this is a top-level property (not nested in another clock context), I would simply write
>
> always (r|=>f)@c abort b
>
> This illustrates the simplicity of using the clock expression (or not) to make abort synchronous (or not). And although the syntax gets more 'twisted' when abort is nested within an outer clock context, and you want to switch clocks or hide them altogether, the same is already true of all other operators! So this is NOT a special case with abort - rather, making abort NOT sensitive to the clock context has created a special case, unnecessarily.
>
> In any case, the properties I've seen people write rarely involve a nested abort, so this issue of 'twisted' syntax is very unlikely to occur. The one possible issue that I see if abort were to be sensitive to the clock context is that use of a default clock declaration and an asynchronous abort would be in conflict, because the @True required to make the abort asynchronous would shield the property from the default clock context. But I would argue that a default clock declaration strongly implies that we are dealing with a single-clock, synchronous system, and I would expect ALL properties to be affected uniformly by that single clock. I would not expect abort to ignore that clock.
>
> With regard to until vs. abort, I understand the semantic differences - but most users do not. Users learning the language for the first time typically get confused between abort and until, because (in their view) the semantics are almost the same. In my opinion, it would be best if there were a single, fundamental difference (canceling outstanding 'partial satisfactions' vs. canceling any obligation to be satisfied in the present/future) rather than two. Learning that the abort condition is insensitive to the clock context will lead some users to think that the until condition is similarly insensitive to the clock.
>
> The bottom line is that languages should be orthogonal unless there is a very good reason not to be. The argument that abort is designed to model asynchronous reset is not a sufficiently good reason, because users are not using it only for that purpose; they are also using it for synchronous reset/interrupt/etc. signals.
>
> Regards,
>
> Erich
>
> | -----Original Message-----
> | From: Johan Mårtensson [mailto:johan.martensson@safelogic.se]
> | Sent: Thursday, December 16, 2004 4:26 AM
> | To: ieee-1850-extensions@eda.org; Erich Marschner
> | Cc: Cindy Eisner; dana.fisman@weizmann.ac.il
> | Subject: Re: Group A - first draft LRM changes
> |
> | Erich,
> |
> | my understanding is that abort has an 'asynchronous'
> | definition for a reason, and that is that it is meant to be
> | used to disable properties in case there is a reset. In the
> | general case we cannot make any assumptions on when a reset
> | can occur, especially we cannot assume that resets occur only
> | on clock flanks. With a 'synchronous only' definition for
> | abort as you suggest you would have a default behavior where
> | resets that are 'visible' to the design would be 'invisible'
> | to the property.
> | It is clear that you want to treat reset and set signals
> | differently from others when dffs are concerned. With regard
> | to other signals it is only their value at the clock flank
> | that will influence the state of the circuit whereas reset
> | and set signals will affect the state regardless on when they
> | occur. Because of this there is in my view a strong case for
> | treating aborts asynchronously.
> |
> | In what cases would your definition have an advantage?
> | Presumably in cases where you want the property to be aborted
> | only when the abort signal occurs at a clock flank but not if
> | it occurs otherwise. Is there really a demand for this? If
> | there is we could perhaps add a sych_abort construct to the
> | language with your definition.
> |
> | If we instead change the definition of abort as you suggest
> | then -- apart from nasty backwards compatibility issues which
> | should not be taken lightly -- users that would like to use
> | abort for handling resets in the way described above would
> | have to write 'twisted' things like.
> |
> | (always r|=>(f@c abort b)@TRUE)@c
> |
> | for what is currently expressed by
> |
> | (always r|=>f abort b)@c
> |
> | Also, I don't think your comparison with until is to the
> | point. Until is meant to describe behaviour that is trigged
> | at each clock cycle until a certain condition obtains. The
> | semantics of 'F until b' is very different from 'F abort b'
> | even if we ignore the asyncronous/synchronous issue.
> |
> | 'F until b' means that F is asserted at every instance up
> | until the first instance where b is true. The different
> | instances of F are in no sence aborted by the occurrence of
> | b. This means that the formula 'F until b' may require things
> | from the model beyond the occurrence of b.
> |
> | 'F abort b' instead asserts only one instance of F at the
> | first cycle and it is true if F is not contradicted
> | operationally at the first time when b is true. This means
> | among other things that nothing is required of the model
> | beyond the occurrence of b.
> |
> | 'until' is thus not suited for modeling resets in the way abort is.
> |
> | Best Regards, Johan M
> |
> |
> | On Wed, Dec 15, 2004 at 02:09:53PM -0800, Erich Marschner wrote:
> | > 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
> | > | ------------------------------------------------------------
> | > |
> | > |
> | > |
> |
> | --
> | ------------------------------------------------------------
> | 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
------------------------------------------------------------