Subject: [sv-ac] Cyclicity issues
From: Joseph Lu (Juin-Yeu.Lu@sun.com)
Date: Wed Feb 12 2003 - 18:16:26 PST
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 - 18:17:10 PST