Subject: RE: [sv-ac] cyclicity and ill-founded forms
From: Bassam Tabbara (bassam@novas.com)
Date: Thu Feb 13 2003 - 08:37:07 PST
Hi Cindy,
I meant "[...after the doc explains how named sequence instantiation in
another definition works] we can add the wording that explains that an
error will be flagged when there is a cycle in the spec definitions"
Thx.
-Bassam.
-- Dr. Bassam Tabbara Technical Manager, R&D Novas Software, Inc.http://www.novas.com (408) 467-7893
> -----Original Message----- > From: Cindy Eisner [mailto:EISNER@il.ibm.com] > Sent: Thursday, February 13, 2003 4:51 AM > To: bassam@novas.com > Cc: 'Erich Marschner'; bassam@novas.com; 'Jay Lawrence'; > john.havlicek@motorola.com; Surrendra.Dudani@synopsys.com; > sv-ac@eda.org > Subject: RE: [sv-ac] cyclicity and ill-founded forms > > > bassam, > > i agree with everything you said, except that i don't > understand what this > means: > > >Then it would be adequate to add > >the -definition cycle- semantic check > > i don't want to lead everyone down another minor branch of > the advanced semantics, so if you feel the above is not > important, there is no need to answer, and we can focus on this: > > >** We better clean up what the doc means about > "instantiating a named > >sequence" and what the semantics are. > > 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 > > > "Bassam Tabbara" <bassam@novas.com> on 12/02/2003 17:34:32 > > Please respond to <bassam@novas.com> > > To: Cindy Eisner/Haifa/IBM@IBMIL, "'Erich Marschner'" > <erichm@cadence.com>, <bassam@novas.com> > cc: "'Jay Lawrence'" <lawrence@cadence.com>, > <john.havlicek@motorola.com>, <Surrendra.Dudani@synopsys.com>, > <sv-ac@eda.org> > Subject: RE: [sv-ac] cyclicity and ill-founded forms > > > > 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 : Thu Feb 13 2003 - 08:37:58 PST