Re: [$ieee-1850] multi-clocked suffix implications

From: ben cohen <hdlcohen@gmail.com>
Date: Tue Jan 04 2005 - 08:47:02 PST

Cindy,
My point is that the "@cx" reads as "at clock x", implying validity
of "a" only at the transition. Whereas {a}@c1 |-> {b}@c2 states
that at transition of "a", "b" must be valid at that time, AND at the
next clock c2 (?).
That is where my confusion comes from.
In any case, we need to embellish the note with some explanations,
otherwise, users like me would me confused. Am I alone on this?
Thanks for your detailed explanations,
Ben

On Tue, 4 Jan 2005 06:35:45 -0800, Erich Marschner <erichm@cadence.com> wrote:
> Ben,
>
> I want to clarify an important point. The IEEE 1850 PSL working group is not required to "be in sync with SVA" to the point of removing capabilities that are not present in SVA. So there is no reason for you to suggest that we remove capabilities in PSL just because they don't exist in SVA.
>
> In any case, I believe the semantics are quite clear. In the case you give below, you have an unclocked |-> property with a clocked LHS and a clocked RHS, so the semantics of unclocked |-> apply at the top level, and the semantics of clocked sequences apply to the LHS and RHS. The transition from the end of the LHS to the beginning of the RHS is therefore governed by the semantics of unclocked |->. Those semantics require that the RHS must 'start' in the same state in which the LHS completes.
>
> I gather that you think having different clocks on the LHS and the RHS would make this impossible, but I don't believe that is true. If I understand the semantics correctly, the RHS sequence can hold tightly starting from that state, even though its clock may not occur until later. For example, clearly the following would be satisfiable:
>
> {a}@c1 |-> {[*]@true;b}@c2
>
> but so also would
>
> {a}@c1 |-> {[*];b}@c2
>
> and even
>
> {a}@c1 |-> {b}@c2
>
> because, for a clocked SERE to hold tightly, its first element must hold tightly under the clock context, and this reduces to holding tightly on a path that is a clock tick of the clock (i.e., it allows for the clock to occur later than the first cycle of the path).
>
> So I see no reason to exclude this capability from PSL.
>
> Regards,
>
> Erich
>
> | -----Original Message-----
> | From: owner-ieee-1850@eda.org
> | [mailto:owner-ieee-1850@eda.org] On Behalf Of ben cohen
> | Sent: Tuesday, January 04, 2005 9:06 AM
> | To: Cindy Eisner
> | Cc: Harry D Foster; ieee-1850-lrm@eda.org; ieee-1850@eda.org
> | Subject: Re: [$ieee-1850] multi-clocked suffix implications
> |
> | 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 08:47:32 2005

This archive was generated by hypermail 2.1.8 : Tue Jan 04 2005 - 08:47:42 PST