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
------------------------------------------------------------