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

Hi Ben/Eric,
Actually, there is no difference in semantics of SVA and PSL with respect
to the implication operators:
|->(overlapping), and |=> (non-overlapping), and as Eric mentioned |=> is
derived from |-> as

  r |=> phi === {r; true} |-> phi
However, the above translation is true for unclocked expressions, and
happens to be true for singly clocked expressions, but for multi-clocked
expressions,
{a}@c1 |=> {b}@c2
is not equivalent to
{a; true}@c1 |-> {b}@c2
but is equivalent to
{a}@c1 ; true |-> {b}@c2
meaning, a is at clock c1, true is unclocked(clocked at the finest
granularity), and b is at the clock c2.

We refer to |=> as non-overlapping because there is always some time gap
between antecedent and consequent. When a is true at c1, b must be true at
the first tick of c2 AFTER c1, even if c1 and c2 are coincident at that
point in time. (I'm assuming a and b be are just booleans)

If the formula was
{a}@c1 |-> {b}@c2
then there may not be any gap between the antecedent and consequent. When a
is true at c1, b must be true at the first tick of c2 starting from that
point in time. This may result in no time gap if c1 and c2 happen to be
coincident at that point. Otherwise, there will be some gap until c2
becomes true.
Please note that {a}@c1 |-> {b}@c2 and {a}@c1 |=> {b}@c2 will result in
identical evaluations if c1 and c2 were never coincident when a is true.

In SVA, the use of overlapping |-> for multi-clocks is disallowed because
of the unsynthesizable nature of detecting coincident edges of two
different clocks.

Surrendra

At 01:19 PM 1/4/2005 -0800, Erich Marschner wrote:
>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
>| --------------------------------------------------------------
>| -------------
>|
>|

**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive, Suite 300
Marlboro, MA 01752

Tel: 508-263-8072
Fax: 508-263-8123
email: Surrendra.Dudani@synopsys.com
**********************************************
Received on Wed Jan 5 09:21:49 2005