Re: [sv-ac] alternative proposal to "syn1": remove binary delay


Subject: Re: [sv-ac] alternative proposal to "syn1": remove binary delay
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Wed Feb 12 2003 - 05:45:09 PST


surrendra,

>The meaning of a subsequence
>changes depending upon its use as a unary or a binary.

i disagree. the one thing that both "syn1" and my alternative proposal to
"syn1" have in common is that both have only one kind of delay. in "syn1"
there is only binary delay. in the alternative proposal there is only
unary delay, which i have preferred to rename as "start-at".

>In addition,
>
>a ; ([1] b) means the same as a ;[1] b
>but,
>a ; ([0] b) is disallowed, although a;[0] b is allowed

yes. in general, "a ; ([n] b)" means the same as "a ; [n] b", which is the
beauty of both proposals. the disadvantage of "syn1" is that it does not
allow a leading delay, as in: "[n] a". the disadvantage of the aternative
is that "[0] a" is not allowed. in effect, the the [0] has become part of
the ";" operator, rather than being considered as a delay.

the advantage of both is that parentheses are not invested with any
semantic meaning.

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

"dudani@us04.synopsys.com" <Surrendra.Dudani@synopsys.com>@eda.org on
11/02/2003 19:02:33

Sent by: owner-sv-ac@eda.org

To: sv-ac@eda.org
cc:
Subject: Re: [sv-ac] alternative proposal to "syn1": remove binary
       delay

I have the same concern as Adam pointed out. The meaning of a subsequence
changes depending upon its use as a unary or a binary. In addition,

a ; ([1] b) means the same as a ;[1] b
but,
a ; ([0] b) is disallowed, although a;[0] b is allowed

Surrendra

At 10:40 AM 2/11/2003 -0600, you wrote:

>Hi Cindy;
>
>
>Here are some sequence examples that I would like to see if the
>current proposal works with them.
>
>Specifications:
>1. A and 2 cycles later B
>2. A and 1 or 2 cycles later B
>3. A followed by seqC (seqC is C now or in 10 cycles.)
>4. A implies B (same cycle)
>5. A implies B (in next cycle)
>5. A implies B in the next 1 to 10 cycles.
>
>
>Alternative to syn1:
>
>1. (A; [2] b) ok
>2. (A; [1:2] b) ok
>3. sequence seqC = ([1:10] c);
> (A; seq) missing A&C as legal.
>4. (A => B); ok
>5. (A => [1] B) incorrect.
>6. (A => [1:10] B) missing cycle 10 since A => B is same
cycle.
>
>These can be fixed by rewriting them as:
>
> 3 ???
> 5. (A => [2] B) though seems to say 2 cycles later
> 6. (A => [2:10] B) <same reasoning>
>
>
>LRM 0.79:
>
>1. (A; [2] b) ok
>2. (A; [1:2] b) ok
>3. sequence seqC = ([0:10] c);
> (A; seq) ok.
>4. (A => b); ok
>5. (A => [1] b); ok
>6. (A => ([1:10] b) ok.
>
>
>Is this accurate? How would one rewrite #3 for alternative to syn1 ?
>Which is better?
>
>
> 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 - 05:41:59 PST