Subject: Re: [sv-ac] cyclicity and ill-founded forms
From: John Havlicek (john.havlicek@motorola.com)
Date: Wed Feb 12 2003 - 08:00:24 PST
Erich and All:
A few comments.
> 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 =3D ( clk[*2]; !clk[*3]; ClockSequence )
>
> This seems to be equivalent to the definition
>
> sequence ClockSequence =3D ( clk[*2]; !clk[*3] ) [*inf]
Intuitively, these look equivalent to me, but they seem to be defining
an omega-regular language, not a regular language. I don't think there
is any finite word in the language. Does the SVA LRM allow the analog
of "[*inf]" as a repetition operator? I am under the impression that
only the "*[m:inf]" form of the operator is allowed, where m is finite.
This situation is in contrast to something like
sequence ClockSequence = (clk*[2]; !clk*[3]) or (clk*[2]; !clk*[3]; ClockSequence)
which looks intuitively like
sequence ClockSequence = (clk*[2]; !clk*[3])*[1:inf]
> So I'm not sure what it means to simply ban all "cyclic" constructs. =
> Does that preclude banning such situations as=20
>
> (1; s) =3D> (1; t);
> (1; t) =3D> (1; s);
> ? I don't think we would want to go that far. =20
I agree that this seems to go too far. Note that these are not themselves
_definitions_, but property expressions. What I have been worried about
is ill-founded cyclic definitions. It looks like the issue may be more
subtle than I originally anticipated.
In the CBV proposal to FVTC, we tried to say carefully when cycles are
disallowed, but we had recursive forms, so obviously we didn't say all
cycles are disallowed.
Best regards,
John Havlicek
> 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 =3D ( clk[*2]; !clk[*3]; ClockSequence )
>
> This seems to be equivalent to the definition
>
> sequence ClockSequence =3D ( 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=20
>
> (1; s) =3D> (1; t);
> (1; t) =3D> (1; s);
>
> ? I don't think we would want to go that far. =20
>
> 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=20
>
> | -----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
> | =20
> | =20
> | jay,
> | =20
> | >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.
> | =20
> | but you are talking about cycles in a netlist. the question=20
> | as originally
> | raised was about cycles in a specification. that is something else
> | entirely. in fact, in the context of cycles in a=20
> | specification, i don't
> | understand the whole discussion of syntactic vs. semantic=20
> | cycles. adam
> | showed:
> | =20
> | > seq s =3D (t;x);
> | > seq t =3D (s;y);
> | =20
> | this is a cyclic definition, not a cyclic netlist or a=20
> | combinational loop.
> | what does a semantic cycle mean in this context?
> | =20
> | regards,
> | =20
> | cindy.
> | =20
> | Cindy Eisner
> | Formal Methods Group Tel:=20
> | +972-4-8296-266
> | IBM Haifa Research Laboratory Fax: +972-4-8296-114
> | Haifa 31905, Israel e-mail:
> | eisner@il.ibm.com
> | =20
> | =20
> | "Jay Lawrence" <lawrence@cadence.com>@eda.org on 12/02/2003 14:39:21
> | =20
> | Sent by: owner-sv-ac@eda.org
> | =20
> | =20
> | To: <john.havlicek@motorola.com>
> | cc: <Surrendra.Dudani@synopsys.com>, <sv-ac@eda.org>
> | Subject: RE: [sv-ac] cyclicity and ill-founded forms
> | =20
> | =20
> | =20
> | =20
> | 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=20
> | find a path
> | that violates a timing constraint, but a logical analysis of=20
> | that path
> | may determine that no input sequence will ever cause it to=20
> | fire (or even
> | harder, no VALID input sequence in the protocol).
> | =20
> | 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=20
> | this list
> | can confirm this, I've had this conversation with Kurshan in the =
> past
> | and believe I'm summarizing it properly).
> | =20
> | 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=20
> | runtime, but
> | should probably include verbage that a tool 'may' detect it=20
> | at compile
> | time as well.
> | =20
> | Jay
> | =20
> | =
> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
> | Jay Lawrence
> | Architect - Functional Verification
> | Cadence Design Systems, Inc.
> | (978) 262-6294
> | lawrence@cadence.com
> | =
> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
> | =20
> | > -----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=20
> | 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_=20
> | 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 =3D (t;x);
> | > > > > > seq t =3D (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
> | > > > **********************************************
> | > > >
> | > > >
> | >
> | =20
> | =20
> | =20
> | =20
This archive was generated by hypermail 2b28 : Wed Feb 12 2003 - 08:01:29 PST