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

Hi Eric,
Just to clarify the points you mentioned:
1) Its a good goal to verify asynchronous (unclocked) properties, but for
SVA it was decided to limit to synchronous property checking constructed
out of well formed clocks. In general, users are expected to deploy other
means to validate clocks problems and asynchronous circuits.
2) Action blocks are not part of property verification, and are used for
ancillary functions, such as coverage, testbench reactivity and displaying
messages. That is why there is no requirement for them to be synthesizable.
The code in action blocks is like any other System Verilog code. Users can
always bend the underlying assumptions and write code in action blocks to
modify property behavior. There are other ways of doing the same: calling
tasks/functions from within a property. Also, it was not the intention to
make action blocks part of formal property verification.
3) Regarding derived clocks from parent clocks relates to the problem of
identifying equivalent clocks. It is left up to the tools to provide means
to alias clocks or to analyze RTL to automatically determine such cases.
Future versions of SVA may define equivalent clocks and require tools to
perform analysis.
Surrendra

At 01:44 PM 1/5/2005 -0800, you wrote:
>Surrendra,
>
>Thanks for pointing out my translation error. Yes, the property
>
> 2. {a}@c1 |=> {b}@c2 // ?
>
>is equivalent to
>
> 3. {{a}@c1; true} |-> {b}@c2
>
>rather than
>
> 3. {a; true}@c1 |-> {b}@c2
>
>
>| In SVA, the use of overlapping |-> for multi-clocks is
>| disallowed because of the unsynthesizable nature of detecting
>| coincident edges of two different clocks.
>
>I think it is a bit odd that SVA explicitly disallows |-> in a multi-clock
>property. After all, an action block can contain unsynthesizable
>constructs, so limiting the assertion proper to being synthesizable seems
>inconsistent.
>
>One reason for supporting |-> on multiply-clocked properties is that doing
>so allows us to catch a class of errors associated with clock domain
>crossings. In particular, if the two clocks do not have a fixed
>relationship (i.e., one may drift w.r.t. the other, or even beat against
>the other if they are asynchronous), then it may be that two clock edges
>will occur essentially at the same time, at least as measured by time in
>simulation. Simply disallowing |-> in such cases only guarantees that the
>alternative assertion (using |=>) will never see the case in which the two
>clock edges occur essentially at the same time. This could result in the
>user missing problems that should have been detected.
>
>Also, if c1 and c2 are both derivatives of the same clock tree, and they
>consistently stay in synch, then they are effectively the same
>clock. Since |-> is allowed when the two clocks are identical, I would
>argue that it ought to be allowed when the two clocks behave identically,
>even if they are expressed differently.
>
>Regards,
>
>Erich
>
>| -----Original Message-----
>| From: owner-ieee-1850@eda.org
>| [mailto:owner-ieee-1850@eda.org] On Behalf Of Surrendra Dudani
>| Sent: Wednesday, January 05, 2005 11:57 AM
>| To: ieee-1850@eda.org
>| Subject: 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
>| **********************************************
>|
>|
>|

**********************************************
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 Thu Jan 6 13:01:24 2005