Subject: Re: [sv-ac] Cyclicity issues
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Wed Feb 12 2003 - 23:19:22 PST
joseph,
i don't see a cycle of any kind in your example. can you explain?
thanks,
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>@eda.org on 13/02/2003 04:16:26
Please respond to Joseph Lu <Juin-Yeu.Lu@sun.com>
Sent by: owner-sv-ac@eda.org
To: sv-ac@eda.org
cc:
Subject: [sv-ac] Cyclicity issues
Good evening all,
If we simply disallow syntactic cycles, we are
limiting ourself from proving some design properties
that are specified to ensure the absence of semantic
cycles for the design under test. We need to
remove this limitation.
For example, I define some transaction relations in a
partial-order manner for a concurrent MP system and
and for some conditions, we do not want the observed
behaviors to have a cycle.
seq s = (x;y)
seq t = (y;x)
Property:
assert: if (mode == T) then not(s and t)
where s and t are observed sequences from two
different processors.
Best regards,
--Joseph
--------------------------------------------------
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
--------------------------------------------------
>X-Unix-From: Surrendra.Dudani@synopsys.com Sun Feb 9 19:54:11 2003
>X-Sender: dudani@us04.synopsys.com
>Date: Sun, 09 Feb 2003 22:52:42 -0500
>To: sv-ac@eda.org
>From: "dudani@us04.synopsys.com" <Surrendra.Dudani@synopsys.com>
>Subject: Re: [sv-ac] cyclicity and ill-founded forms
>Mime-Version: 1.0
>
>All acyclic definitions are illegal. LRM should be updated to clearly
state
>this restriction.
>Surrendra
>At 04:36 PM 2/9/2003 -0600, you wrote:
>>sv-ac@eda.org
>
>
>
>**********************************************
>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 - 23:16:27 PST