Subject: RE: [sv-ac] cyclicity and ill-founded forms
From: Jay Lawrence (lawrence@cadence.com)
Date: Wed Feb 12 2003 - 04:39:21 PST
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 - 04:40:09 PST