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


Subject: Re: [sv-ac] alternative proposal to "syn1": remove binary delay
From: Adam Krolnik (krolnik@lsil.com)
Date: Wed Feb 12 2003 - 09:05:31 PST


Hi John, all;

Thanks for the comments, I've corrected the forms below.

>Which is more vile?
> That "s ;([0]t)" is not the same as "s;[0]t",
> That " [1]t" is the same as " t"?

The first is distasteful due to the commonness of parenthesis (even where not necessary.)

The second one is distasteful because of the fact that "[1] t"
looks different in (s; [1] t), vs. (s => [1:10] t).
I.e. the context determines how it works.

Also, you wrote:

>>5. (A => [1] B) incorrect.
>>6. (A => [1:10] B) missing cycle 10 since A => B is same cycle.

>This is a coding mistake. If one adopts the new proposal, one must
>understand that "[1]B" means "B", not "1;B". This is like learning
>to count from 1 instead of from 0. My personal opinion is
>that "[0]B" is more intuitive for "B" than "[1]B".

One other idea to add is:

   "This will be a common mistake that a reviewer would also miss.
    These kind of mistakes are annoying because they are 'close enough'
    but not correct."

My hope is that writing 5 and 6 as shown below moves one away from this
easy misunderstanding.

Okay so on to forms, I've corrected the forms from the original mail:

Specifications:
1. A and 2 cycles later B
2. A and 1 or 2 cycles later B
3. A followed by (overlapping possible) seqC (seqC is C now or in the next 10 cycles.)
4. A implies B (overlapping)
5. A implies B (in next cycle)
6. A implies B in the next 1 to 10 cycles.
7. A implies B (overlapping possible) within the next 10 cycles

Alternative to syn1:

1. (A; [2] b) ok
2. (A; [1:2] b) ok
3. sequence seqC = ([1:10] c);
    (A; [0] seq) ok.
4. (A => B); ok
5. (A => 1; B) ok but *1.
6. (A => 1; [1:10] B) ok but *1
7. (A => [1:11] B) ok *2

Note *1: I've adjusted the form slightly to explicitly show the advance to the next
cycle separate from the sequence we are looking for...
Note *2: This form shows where N must turn into N+1.

LRM 0.79:

1. (A; [2] B) ok
2. (A; [1:2] B) ok
3. sequence seqC = ([0:9] c);
    (A; [0] seq) ok.
4. (A => B); ok
5. (A => [1] B); ok
6. (A => [1:10] B) ok.
7. (A => [0:10] B) ok.

   Thanks John;

    Adam Krolnik
    Verification Mgr.
    LSI Logic Corp.
    Plano TX. 75074



This archive was generated by hypermail 2b28 : Wed Feb 12 2003 - 09:07:43 PST