Cindy,
I have an issue with
"The forms (sere1@clk1 |-> sere2@clk2 " being legal.
In SVA the "|=>" implies synchronization from the endpoint of sere1 to
the first edge of the start of sere2 clocked at clk2. What does "|->"
means in relation to multi-clocks?
That is ambiguous. Where is the synchronization? Which edge?
Also, if we want to be in sync with SVA, I suggest that the "|->" be illegal.
Ben Cohen
On Tue, 4 Jan 2005 14:13:06 +0200, Cindy Eisner <EISNER@il.ibm.com> wrote:
>
>
> 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
>
>
-- -------------------------------------------------------------------------- Ben Cohen Trainer, Consultant, Publisher (310) 721-4830 http://www.vhdlcohen.com/ ben@abv-sva.org * Co-Author: SystemVerilog Assertions Handbook, 2005 ISBN 0-9705394-7-9 * Co-Author: Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0 * Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8 * Component Design by Example ", 2001 isbn 0-9705394-0-1 * VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn 0-7923-8474-1 * VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn 0-7923-8115 ---------------------------------------------------------------------------Received on Tue Jan 4 06:06:15 2005
This archive was generated by hypermail 2.1.8 : Tue Jan 04 2005 - 06:06:17 PST