Subject: Re: [sv-ac] Cyclicity issues
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Sun Feb 16 2003 - 07:47:07 PST
joseph,
>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.
i think that once again we are mixing up two kinds of verification. the
kind of thing you are talking about above is a proof of the static
structure of the design, i think. that is, a proof of the structure of the
netlist. while the kind of verification we are talking about in this
committee is verification of the possible behaviors of a design. so while
a theorem-prover like hol or pvs could find a syntactic cycle, the language
to describe that syntactic cycle would not be the one we are discussing in
this committee.
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
Joseph Lu <Juin-Yeu.Lu@Sun.COM> on 13/02/2003 21:06:12
Please respond to Joseph Lu <Juin-Yeu.Lu@Sun.COM>
To: john.havlicek@motorola.com, Cindy Eisner/Haifa/IBM@IBMIL
cc: sv-ac@eda.org
Subject: Re: [sv-ac] Cyclicity issues
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 : Sun Feb 16 2003 - 07:45:05 PST