Subject: RE: [sv-ac] cyclicity and ill-founded forms
From: Bassam Tabbara (bassam@novas.com)
Date: Wed Feb 12 2003 - 07:34:32 PST
Cindy, first of all I want to commend you on first attempting to ask
about the (current!) defintion of "syntactic/semantic" cycle. The
wording is unfortunate indeed since it is open to fluid interpretation:
"syntactic" initially meant in John's email "definition" as you state
below, and cycles/edges (as John described in detail) meant a def/use
relationship. "semantic" (at least in -my interpretation-) of Jay's
initial question meant a real vs. perceived realization of a def cycle
e.g.
seq s
seq t: precondition => s; // may never happen
I'm afraid this interpretation of mine led to the compile time/runtime
discussion item ...
That's history, I think it would be wrong at this point in time given
the -valid items- that Eric posed to just forgo this thread ... Let me
try to give an opinion on "why we are here and now ?".
** I suspect our document has failed to address the -MEANING- (semantics
:-)!) of what the following is:
seq a;
seq b: x;y;z; a ; // What does the named sequence a here mean
???
So at this point in time, I'd like to step back (forget cycles for a
second, that's a special case of "a" being replaced by "b" in a -simple-
cycle ...) and ask what does the above mean ??
Cindy, also note (correct me here) in PSL we had the clean notion of
instantiating a named sequence. Here this is bypassed (for a
sequence...), in fact the doc introduces things like seq1 ; seq2 even
before we define the named sequence notion !!
I suspect many of us have already looked at PSL and/or OVA and tend to
superimpose the notions from there onto here. But as it stands the doc
itself does not indicate either way:
1) We could just "inline" (a.k.a. instantiate) "a" sequence and
go back to its (design) source signals, in which case the ideas of "def
cycle" would apply when we can't figure out how to do this !
2) In some cases (as Eric's example) our endless inlining may
have a meaning of "endless repetition" so it might make to allow this in
Eric's assertion
3) May be Jay is right, "a" in its second occurrence really
means a latched version of "a"..
4) Many many other possible interpretations here !
** However, (2), (3) (especially this one!) are beyond the scope of the
model of computation we have agreed on for the specification evaluation.
It is an interesting line of thought but I am not sure we have enough
bandwidth to handle this.
** We better clean up what the doc means about "instantiating a named
sequence" and what the semantics are. Then it would be adequate to add
the -definition cycle- semantic check (you need to have the semantics
first before checking it though :-)!!!!!!!!). Also the bit about "ended"
needs to be pulled back here to have a consistent view for how a named
sequence value can be looked up and not inlined (substituted,
instantiated ....).
Hope that was a good wack at refocusing this discussion. Thanks to all,
especially John and Jay for starting this discussion, and Cindy for
asking the right questions. There is no harm in evolving the discussion
but let's table advanced semantics for now and clean up what we started
with so that our users do not get into this confusion!
-Bassam.
P.S. I wonder if we need a designer (who does not know OVA/PSL) to
start fresh on our doc and tell us if its coherent and ask questions
....
-- Dr. Bassam Tabbara Technical Manager, R&D Novas Software, Inc.http://www.novas.com (408) 467-7893
> -----Original Message----- > From: owner-sv-ac@server.eda.org > [mailto:owner-sv-ac@server.eda.org] On Behalf Of Cindy Eisner > Sent: Wednesday, February 12, 2003 6:51 AM > To: Erich Marschner > Cc: Jay Lawrence; john.havlicek@motorola.com; > Surrendra.Dudani@synopsys.com; sv-ac@server.eda.org > Subject: RE: [sv-ac] cyclicity and ill-founded forms > > > > 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 - 07:36:10 PST