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

Erich,
I misunderstood Cindy's statement : " 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." The "starting from
that state" threw me off.

So what is the difference between
1. {a}@c1 |-> {b}@c2 // and
2. {a}@c1 |=> {b}@c2 // ?

Thanks,
Ben

On Tue, 4 Jan 2005 11:59:11 -0800, Erich Marschner <erichm@cadence.com> wrote:
> Ben,
>
> Why do you think that b must be valid at the transition of a as well as at the next tick of c2? That is not what the formal semantic definition says, nor what the informal semantics says, as far as I can see.
>
> If there is any ambiguity at all, it is that the RHS could be taken as either a clocked sequence that is promoted to a property (Clocked_SERE => Sequence => FL_Property), or as an unclocked sequence that is promoted to a property and then clocked (Braced_SERE => Sequence => FL_Property, and FL_Property@clk => FL_Property). Either way, I believe the semantics end up being the same.
>
> In both cases, the semantics come down to the first boolean in the sequence holding at the end of the first 'clock tick' of c2 - i.e., at the first occurrence of c2. The boolean does NOT need to hold in the first cycle of the path, if c2 does not hold there; it only needs to hold in the first cycle in which c2 holds.
>
> The informal semantics of clocked sequences (though flawed in other ways) also make this clear. The current definition says
>
> For unclocked SERE A and Boolean CLK:
>
> A@CLK holds tightly on a given path iff (if and only if) CLK holds
> in the last cycle of the given path, and A holds tightly on the path
> obtained by extracting from the given path exactly those cycles in
> which CLK holds.
>
> Although this definition is being improved to handle nested clocks, it is sufficient for this example. The discussion of 'extracting' states in which the clock holds should make it clear that {b}c2 holds on a given path provided only that b holds on the first cycle of that path in which c2 holds. So given the property {a}@c1 |-> {b}@c2, the RHS will hold on the path starting with the state in which {a}@c1 completes, provided only that b holds in the first cycle (of that path) in which c2 holds - i.e., the that b holds in the first cycle in which c2 holds, at or after the completion of {a}@c1.
>
> There is no requirement for b to hold in the same cycle in which a holds, which is not surprising, since a and b are on different clocks.
>
> I hope this helps.
>
> Regards,
>
> Erich
>
> | -----Original Message-----
> | From: ben cohen [mailto:hdlcohen@gmail.com]
> | Sent: Tuesday, January 04, 2005 11:47 AM
> | To: Erich Marschner
> | Cc: Cindy Eisner; Harry D Foster; ieee-1850-lrm@eda.org;
> | ieee-1850@eda.org
> | Subject: Re: [$ieee-1850] multi-clocked suffix implications
> |
> | 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
> | > | --------------------------------------------------------------
> | > | -------------
> | > |
> | > |
> | >
> |
> |
>

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