RE: Group A - first draft LRM changes

Johan,

Thanks for pointing out my error. Given the fuzziness of the current Appendix B, I tend to misread the ||= symbol (for Boolean satisfaction) as |=.

So let me restate my suggestion. Instead of

   v^j ||= b

we could define this as

   v^j ||= (b 'and' c)

or

   v^j ||= c and v^j ||= b

or something equivalent. The point is that it should be possible to define clocked abort so that the boolean condition is considered only when it occurs in conjuction with the clock context. And such a definition would be much more consistent with the rest of the language.

Regards,

Erich
 

| -----Original Message-----
| From: Johan Mårtensson [mailto:johan.martensson@safelogic.se]
| Sent: Wednesday, December 15, 2004 2:29 PM
| To: ieee-1850-extensions@eda.org; Erich Marschner
| Cc: bassam@novas.com; Johan Mårtensson; Cindy Eisner;
| dana.fisman@weizmann.ac.il
| Subject: Re: Group A - first draft LRM changes
|
| Erich,
|
|
| 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
|
| yes, and what does that mean??? Observe that v^j is a single letter!
|
| /Johan M
| >
| > 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. 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 Wed Dec 15 12:17:34 2004