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