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