RE: Group A - first draft LRM changes

Johan,

Now I understand your example. Thanks for the explanation.

Yes, you can accomplish what I am looking for by 'and'ing the clock with the abort expression. But I don't agree that this is 'easiest'. In particular, it calls into question how many other places the language might require me to do something special to react to the clock, rather than simply using a clock expression. From the point of view of novices (even semi-experts, like me - I have to admit to being quite surprised to learn that abort is always asynchronous) this special case makes it more difficult to learn and use the language effectively. Yes, I can read the formal semantics definition closely to find out if there are any more special cases (I've just done so), but most users will not bother with that; instead they will be left wondering, which will make them less comfortable with the language.

A particular point here is that abort and until are very similar, especially when you take into account the Simple Subset restriction that the RHS operator of until be a Boolean. For until, the clock context affects the RHS Boolean, but for abort it does not. This kind of seemingly arbitrary difference makes the language more difficult to learn and use correctly.

Regards,

Erich

| -----Original Message-----
| From: Johan Mårtensson [mailto:johan.martensson@safelogic.se]
| Sent: Wednesday, December 15, 2004 2:22 PM
| 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,
|
|
| > On Wed, Dec 15, 2004 at 08:37:11AM -0800, Erich Marschner wrote:
| > 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
|
| No, I indeed meant 'b abort a'
|
| with v definied by
|
|
| t: 0123456....
| a: 0100000....
| b: 0000000....
| c: 0010010....
|
| we have
|
| v|= (b abort a)@c
|
| because although b is not true at the first clock occurrence
| the property is true because it is aborted asynchronously by
| an occurrence of a before that.
|
| but
| not v|c |= b abort a
|
| since a is not "visible" when we evaluate only on states
| where c holds:
|
| t: 25....
| a: 00....
| b: 00....
| c: 11....
|
|
| With regard to the need to specify synchronous aborts that
| you describe, isn't the easiest way to just use conjunction
| in the abort boolean.
| Using your example one would write:
|
| always (a -> b abort (c&clk))@clk
|
| to disallow asynchronous abort. Is this what you wanted to achieve?
|
| Best Regards, Johan M
|
|
| > 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
| >
|
|
| > | 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
|
| >
| >
| >
| >
| > | -----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 Wed Dec 15 13:11:57 2004