RE: Group A - first draft LRM changes

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
| ------------------------------------------------------------
|
|
|
Received on Wed Dec 15 07:22:58 2004