Subject: RE: [sv-ac] cyclicity and ill-founded forms
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Wed Feb 12 2003 - 06:50:37 PST
erich,
>So I'm not sure what it means to simply ban all "cyclic" constructs. Does
that preclude banning such >situations as
>
> (1; s) => (1; t);
> (1; t) => (1; s);
>
>? I don't think we would want to go that far.
no, of course not! i should not have used the term "cyclic specification",
but rather "cyclic definition". there should be no cyclic definitions,
like the one that john originally showed:
> seq s = (t;x);
> seq t = (s;y);
when talking about a cyclic definition, i believe that it makes no sense to
make a distinction between compile-time and run-time, or syntactic and
semantic cycles, etc. thus, i think we have been making a mountain out of
a molehill in this discussion.
regards,
cindy.
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-8296-114
Haifa 31905, Israel e-mail:
eisner@il.ibm.com
"Erich Marschner" <erichm@cadence.com> on 12/02/2003 16:27:05
To: Cindy Eisner/Haifa/IBM@IBMIL, "Jay Lawrence" <lawrence@cadence.com>
cc: <john.havlicek@motorola.com>, <Surrendra.Dudani@synopsys.com>,
<sv-ac@eda.org>
Subject: RE: [sv-ac] cyclicity and ill-founded forms
Cindy,
Jay and I were just talking about this ...
In a netlist a 'cycle' means a combinational cycle. A syntactic
(combinational) cycle is one that appears to allow data to propagate in a
cycle - and to stabilize eventually or oscillate depending upon the logic
involved. A semantic (combinational) cycle is one in which such
propagation really can occur. Any semantic cycle is also a syntactic
cycle, but the reverse is not true.
For sequences, which are not strictly combinational, the notion becomes
more interesting. We could presumably define a sequence that refers to
itself, e.g.,
sequence ClockSequence = ( clk[*2]; !clk[*3]; ClockSequence )
This seems to be equivalent to the definition
sequence ClockSequence = ( clk[*2]; !clk[*3] ) [*inf]
Is this a 'syntactic cycle'? It would appear so, because it is
self-referential. Is it a 'semantic cycle'? Not a combinational semantic
cycle, in the sense used in simulation.
So I'm not sure what it means to simply ban all "cyclic" constructs. Does
that preclude banning such situations as
(1; s) => (1; t);
(1; t) => (1; s);
? I don't think we would want to go that far.
Regards,
Erich
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
| -----Original Message-----
| From: Cindy Eisner [mailto:EISNER@il.ibm.com]
| Sent: Wednesday, February 12, 2003 9:06 AM
| To: Jay Lawrence
| Cc: john.havlicek@motorola.com; Surrendra.Dudani@synopsys.com;
| sv-ac@eda.org
| Subject: RE: [sv-ac] cyclicity and ill-founded forms
|
|
| jay,
|
| >The problem here is that syntactic cycles are relatively common and
| >sometimes useful. Being primarily a simulation guy, I think of this
| >problem in terms of combinational cycles and/or false-paths in a
| >gate-level netlist.
|
| but you are talking about cycles in a netlist. the question
| as originally
| raised was about cycles in a specification. that is something else
| entirely. in fact, in the context of cycles in a
| specification, i don't
| understand the whole discussion of syntactic vs. semantic
| cycles. adam
| showed:
|
| > seq s = (t;x);
| > seq t = (s;y);
|
| this is a cyclic definition, not a cyclic netlist or a
| combinational loop.
| what does a semantic cycle mean in this context?
|
| regards,
|
| cindy.
|
| Cindy Eisner
| Formal Methods Group Tel:
| +972-4-8296-266
| IBM Haifa Research Laboratory Fax: +972-4-8296-114
| Haifa 31905, Israel e-mail:
| eisner@il.ibm.com
|
|
| "Jay Lawrence" <lawrence@cadence.com>@eda.org on 12/02/2003 14:39:21
|
| Sent by: owner-sv-ac@eda.org
|
|
| To: <john.havlicek@motorola.com>
| cc: <Surrendra.Dudani@synopsys.com>, <sv-ac@eda.org>
| Subject: RE: [sv-ac] cyclicity and ill-founded forms
|
|
|
|
| The problem here is that syntactic cycles are relatively common and
| sometimes useful. Being primarily a simulation guy, I think of this
| problem in terms of combinational cycles and/or false-paths in a
| gate-level netlist. A structural loop may exist in a combinational
| network, but it may be guaranteed to settle in one iteration (think
| flip-flop). This is downright useful. A timing analyzer may
| find a path
| that violates a timing constraint, but a logical analysis of
| that path
| may determine that no input sequence will ever cause it to
| fire (or even
| harder, no VALID input sequence in the protocol).
|
| I believe that determining that a syntactic loop is in fact
| semantically
| possible, especially in the presence of constraints on the inputs, is
| roughly equivalent to model checking the circuit therefore not always
| computable statically. (Hopefully one of the formal gurus on
| this list
| can confirm this, I've had this conversation with Kurshan in the past
| and believe I'm summarizing it properly).
|
| In cases like this where the easy cases can be handled statically but
| the hard ones can only be detected at runtime, I believe that the
| standard can only say that it 'shall' perform the check at
| runtime, but
| should probably include verbage that a tool 'may' detect it
| at compile
| time as well.
|
| Jay
|
| ===================================
| Jay Lawrence
| Architect - Functional Verification
| Cadence Design Systems, Inc.
| (978) 262-6294
| lawrence@cadence.com
| ===================================
|
| > -----Original Message-----
| > From: John Havlicek [mailto:john.havlicek@motorola.com]
| > Sent: Wednesday, February 12, 2003 2:09 AM
| > To: Jay Lawrence
| > Cc: Surrendra.Dudani@synopsys.com; sv-ac@eda.org
| > Subject: Re: [sv-ac] cyclicity and ill-founded forms
| >
| >
| > I had "syntactic cycles" in mind with my original question.
| >
| > I have been thinking about definitions of elements like sequences,
| > where the syntactic cycles correspond to mutually recursive forms
| > that may be ill-founded. In any case, the mutually recursive
| > forms struck me as beyond the scope of what was intended.
| >
| > J.H.
| >
| > >
| > > Does this mean "semantic cycles" or "syntactic cycles".
| > Simple cycles in
| > > the syntax are not necessarily going to ever occur semantically.
| > >
| > > Jay
| > >
| > > > -----Original Message-----
| > > > From: dudani@us04.synopsys.com
| > [mailto:Surrendra.Dudani@synopsys.com]
| > > > Sent: Tuesday, February 11, 2003 11:45 AM
| > > > To: sv-ac@eda.org
| > > > Subject: Re: [sv-ac] cyclicity and ill-founded forms
| > > >
| > > >
| > > > John is correct. All "cyclic_definitions" are disallowed. LRM
| > > > needs to
| > > > state this restriction.
| > > > Surrendra
| > > > At 10:23 AM 2/10/2003 -0600, you wrote:
| > > > >Hi Adam:
| > > > >
| > > > >The example I gave has a cyclic syntactic dependency.
| > > > >s depends syntactically on t and x, while t depends
| syntactically
| > > > >on s and y. If you form a directed graph from the relation
| > > > >"depends syntactically on", that graph will have a cycle
| > for these
| > > > >definitions.
| > > > >
| > > > >I think Surrendra meant to say that all _cyclic_
| definitions are
| > > > >illegal.
| > > > >
| > > > >Best regards,
| > > > >
| > > > >John Havlicek
| > > > >
| > > > > > Good morning all;
| > > > > >
| > > > > > John wrote:
| > > > > >
| > > > > > I have not yet found any place in the LRM that mentions
| > > > > > acyclicity requirements for defined forms. Without
| > > > > > acyclicity, simple ill-founded forms are possible, e.g.
| > > > > >
| > > > > > seq s = (t;x);
| > > > > > seq t = (s;y);
| > > > > >
| > > > > > Is it intended that all cyclic syntactic dependencies be
| > > > > > disallowed?
| > > > > >
| > > > > > Surrendra wrote:
| > > > > >
| > > > > > All acyclic definitions are illegal. LRM should be
| > updated to
| > > > > clearly state this
| > > > > > restriction.
| > > > > >
| > > > > >
| > > > > > In addition an example should be provided for those not
| > > > currently using
| > > > > terms
| > > > > > such as 'acyclicity'...
| > > > > >
| > > > > >
| > > > > > Adam Krolnik
| > > > > > Verification Mgr.
| > > > > > LSI Logic Corp.
| > > > > > Plano TX. 75074
| > > > > >
| > > > > >
| > > >
| > > >
| > > >
| > > > **********************************************
| > > > Surrendra A. Dudani
| > > > Synopsys, Inc.
| > > > 377 Simarano Drive
| > > > Suite 300
| > > > Marlboro, MA 01752
| > > >
| > > > Tel: 508-263-8072
| > > > Fax: 508-263-8123
| > > > email: dudani@synopsys.com
| > > > **********************************************
| > > >
| > > >
| >
|
|
|
|
This archive was generated by hypermail 2b28 : Wed Feb 12 2003 - 06:48:08 PST