Subject: Re: [sv-ac] Cyclicity issues
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Feb 13 2003 - 13:06:34 PST
Hi Joseph:
> Are the issues that we are concerned here are only related to
> syntactic parsing complication ? Maybe i missing something.
I am coming at this from a semantics perspective. Based on
the intuitive descriptions in the LRM, my expectation is that
the intended semantics for a sequence is a regular language of
finite words.
If we have a recursive definition of a sequence with no way to
"bottom out", then it is not obvious to me how it defines a
language of finite words. With your tail recursion example
seq s = (x;y;s)
my impression is that only infinite words match the pattern
specified by s. Similarly for your head recursion example, although
in this case the situation is stranger because the infinite words
that match are infinite in reverse time rather than forward
time.
It's not clear to me that your example property falls within the
scope of what can be expressed in SVA. It will help me understand
if you can give a more concrete/intuitive description of the
property that is to be represented.
Best regards,
John Havlicek
> Hi John,
>
> Thanks for the comments. Yes, as far as the BFN is concerned, my previous example
> does not have non-terminal terms hanging around in the right-hand side
> of seq declaration which causes a syntactic cycle.
> But I do have an intent to define a syntactic cycle and prove its
> absence in my design. Theorem-provers like HOL and PVS allow me to do that.
>
> Let me reiterate another example which is similar to your previous example.
> This example has a tail or head recursive definition for the sequential
> declaration.
>
> seq s = (x;y;s) // tail recursive
>
> seq s = (s;x;y) // head recursive
>
> assert: if (mode == T) then not(s)
>
> From your example,
>
> seq s = (t;x)
> seq t = (s;y)
>
> they can be translated to head recursions.
>
> seq s = (s;y;x)
> seq t = (t;x;y)
>
> Are the issues that we are concerned here are only related to
> syntactic parsing complication ? Maybe i missing something.
>
> Thanks and best regards,
>
> --Joseph
>
>
>
>
>
> >Date: Thu, 13 Feb 2003 07:55:19 -0600 (CST)
> >To: Juin-Yeu.Lu@sun.com
> >CC: sv-ac@eda.org
> >Subject: Re: [sv-ac] Cyclicity issues
> >From: John Havlicek <john.havlicek@motorola.com>
> >
> >Hi Joseph:
> >
> >> seq s = (x;y)
> >> seq t = (y;x)
> >>
> >> Property:
> >>
> >> assert: if (mode == T) then not(s and t)
> >
> >I see no problem with these definitions. I would not
> >call them cyclic. The "syntactic dependency graph" for
> >them looks like
> >
> > s -----> x <----- t
> > | |
> > ----> y <----
> >
> >which is not cyclic (as a directed graph).
> >
> >Best regards,
> >
> >John Havlicek
>
>
> --------------------------------------------------
> Joseph Lu, Ph.D.
> Global Validation, Processor Product Group
> Sun Microsystems
> M/S USUN 03-202, 430 N. Mary Ave.,
> Sunnyvale, CA 94086
> 408-616-5887
> joseph@eng.sun.com
> --------------------------------------------------
>
>
This archive was generated by hypermail 2b28 : Thu Feb 13 2003 - 13:09:33 PST