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

Ben,

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

Actually, that was my (earlier) reply, not Cindy's.

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

According to the last definition under B.3.2, Additional FL operators, which says that

    r |=> phi === {r; true} |=> phi

property 2 above is equivalent to

  3. {a; true}@c1 |-> {b}@c2

So you can see that the difference between 1 and 2/3 is very slight: they may give different answers only if c2 holds in the same cycle as c1, and {a}@c1 finishes in that cycle. In that case, property 1 would require b to hold immediately, at the immediately occurring tick of c2 coincident with a@c1, whereas property 2/3 would require b to hold in a later cycle at the next tick of c2 after a@c1 occurred.

Regards,

Erich

| -----Original Message-----
| From: ben cohen [mailto:hdlcohen@gmail.com]
| Sent: Tuesday, January 04, 2005 3:10 PM
| 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
|
| 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
| --------------------------------------------------------------
| -------------
|
|
Received on Tue Jan 4 13:20:01 2005