Subject: Re: [sv-ac] alternative proposal to "syn1": remove binary delay
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Wed Feb 12 2003 - 05:40:28 PST
adam,
i see that john has responded. i basically agree with what he said. i
would like to put it in my own words.
3. assuming you want seqC to start within a time window of 10 cycles from
the cycle where A ends, including the cycle where A ends, you would code:
sequence seqC = ([1:10] c);
(A;[0] seqC)
i agree with your solutions to 5 & 6, and i agree that they are ugly. that
is one reason why i would like to see two separate sequence implication
operators, one which says "starting on the same cycle" and the other which
says "starting on the next cycle".
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
Adam Krolnik <krolnik@lsil.com> on 11/02/2003 18:40:48
To: Cindy Eisner/Haifa/IBM@IBMIL
cc: sv-ac@eda.org
Subject: Re: [sv-ac] alternative proposal to "syn1": remove binary
delay
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
This archive was generated by hypermail 2b28 : Wed Feb 12 2003 - 05:37:24 PST