[$ieee-1850] multi-clocked suffix implications

harry,

as a result of a recent discussion on the verification guild:

http://verificationguild.com/modules.php?name=Forums&file=viewtopic&p=2467#2467

i believe that we need to add clarifying text to the lrm that makes it
clear that the form (sere1@clk1 |=> sere2@clk2) is a legal psl property.
note that this is a matter of user-friendliness rather than of correctness,
as the information is available in the lrm, but is not called out to the
casual reader. in order for the reader to understand that this is allowed,
she must traverse the lrm like this:

>see p. 68 of lrm v1.1. one of the options shown for an fl property is
>
>>Sequence |=> FL_Property
>
>a sequence, according to p. 46, can be a clocked sere. and so can an fl
property (because an fl property can be a sequence, see p. 56).

rather than find the information in one central location. i'm thinking of
something like:

NOTE: The forms (sere1@clk1 |-> sere2@clk2 and sere1@clk1 |=> sere2@clk2)
are legal PSL properties, because a clocked SERE is a Sequence, and a
Sequence in turn is an FL Property, and can thus be parsed using the
grammar rules FL_Property ::= Sequence |-> FL_Property and FL_Property ::=
Sequence |=> FL_Property.

i'm not sure where to do this. it seems that the logical place is in
section 6.2.1.6.1 (suffix implication). however, while logical, that might
not be the best place for a reader, who might expect to find the
information in a section called "clocking" or some such.

does anyone have an idea where to incorporate such text? perhaps we need a
clarifying section that summarizes all the places where a clock can be
used?

regards,

cindy.

--------------------------------------------------------------------
Cindy Eisner
Formal Methods Group
IBM Haifa Research Laboratory
Haifa 31905, Israel
Tel: +972-4-8296-266
Fax: +972-4-8296-114
e-mail: eisner@il.ibm.com
Received on Tue Jan 4 04:15:52 2005