Subject: Re: [sv-ac] parsing problem
From: John Havlicek (john.havlicek@motorola.com)
Date: Wed Dec 17 2003 - 08:24:12 PST
Hi Bassam:
I'm sorry this message is long, but I have tried to make sure
I explain my points and give examples. Thanks for your patience.
> Hey John,
>
> I tried to follow your argument in your email, and while the argument
> seems correct, the premise is another matter:
> > (1') @(c) s ##n @(c) t
> >
> > means the same thing as
> >
> > (2') @(c) s ##n 1 ## @(c) t <<<<<<< means: @c s ##n
> "true" ##0 [@c] t
> >
> > in 3.1, and it definitely does not mean the same thing as <<<<<<<<
> not ??
> >
> > (2'') @(c) s ##n t <<<<<<< @c s ##n [1 ##0]
> t
>
> Seems to me it *does* mean the same thing if you interpret ## to be ##0.
There is already a defined semantics for
(2') @(c) s ##n 1 ## @(c) t
in 3.1. In 3.1, (2') is equivalent to
@(c) s ##n 1 ##1 t
In 3.1, (2') is not equivalent to
@(c) s ##n 1 ##0 t
In 3.1, both
@(c) s ##n 1 ##1 @(c) t
and
@(c) s ##n 1 ##0 @(c) t
are illegal syntax. Do you agree?
> I guess I am really missing the finer distinction... actually reading
> the following paragraph in your original email, the last paragraph seems
> to support a ##0 instead of a ##1:
>
> > > > The intuition for "##n", n > 0, in any sequence, whether
> > singly- or
> > > > multiply-clocked, is then the following:
> > > >
> > > > s ##n t
> > > >
> > > > means that from the ending point of s, there are n clock tick
> > > > advances to get to the starting point of t. The first
> > n-1 of these
> > > > advances are to clock ticks of the ending clock of s,
> > while the last
> > > > advance is to a clock tick of the leading clock of t.
>
> In that "last cycle" if t is a different clock then I am really heading
> to the "clock" edge to catch t, if I change that clock, I really need a
> "##0", otherwise I am skipping a beat. Anyway, I can't put my finger on
> the fine point here, may be it is because the premise above... does not
> come across to me.
I am trying to make sure we have a consistency in the semantics
so that we don't have a "semantic jump" when the clocks become the same.
Let's suppose x,y are booleans and c and d are distinct clock events.
In 3.1, to match
@(c) x ## @(d) y
there are two clock ticks:
c d
x y
where by this notation I mean the first is a tick of c, at which x must
be true, and the second is the next strictly subsequent tick of d, at
which y must be true.
Similarly, to match
@(c) x ## @(c) y
there are two clock ticks:
c c
x y
Thus, in 3.1,
@(c) x ## @(c) y
is equivalent to
@(c) x ##1 y
[cf. p. 177 in the 3.1 LRM]. To me, this says that in 3.1 "##" is interpreted
as "##1" when the clocks are the same.
In 3.1,
@(c) x ##1 @(c) y
is illegal, but I can get a very close approximation to it by
sequence foo;
@(c) y
endsequence
@(c) x ##1 foo
which is legal. In 3.1, to match this, there are again two clock ticks:
c c
x y
All of this says to me that in 3.1a, to match
@(c) x ##1 @(d) y
there should be two clock ticks:
c d
x y
The beauty of this is that I have a consistent view of the number of
ticks, regardless of whether c and d happen to be the same. This means
that I don't get strange behavior if c and d are syntactically distinct,
but happen to be semantically equivalent.
If I make the match of
@(c) x ##1 @(d) y
have three ticks:
c c d
x y
then I feel compelled also to make the match of
@(c) x ##1 @(c) y
have three ticks:
c c c
x y
Otherwise, we have to teach users that if they write something
like
sequence s1(clk1, clk2);
@(posedge clk1) x ##1 @(posedge clk2) y;
endsequence
wire [0:0] c2 = c1;
sequence s2;
s1(c1,c1);
endsequence
sequence s3;
s1(c1,c2);
endsequence
then s2 matches on two ticks, while s3 matches on three ticks.
Once I make
@(c) x ##1 @(c) y
match on three ticks, the second "@(c)" is no longer redundant, since
@(c) x ##1 y
still matches on two ticks:
c c
x y
Then in
sequence foo;
@(c) y
endsequence
sequence foo2;
y
endsequence
sequence s4;
@(c) x ##1 foo;
endsequence
sequence s5;
@(c) x ##1 foo2;
endsequence
s4 matches on three ticks (unlike in 3.1), while s5 matches on two ticks.
What this means is that "@(c)" itself is carrying a temporal advance
to the next strictly future tick of c. This takes us out of semantic
alignment with PSL 1.1, where the clock is strengthless and does not
itself account for any temporal advance. We would also have to say
in the formal semantics whether the tick of c is required to exist,
i.e., we have to decide whether "@(c)" is a strong or a weak clock.
I don't think we should do this.
>
> Thx.
> -Bassam.
>
> P.S. I did have 2 threads in my last response, one motivating the ##0
> (instead of the suggested ##1 replacement for "##"), and another for
> "status quo"... Assuming the change is confusing to people.
I've tried to argue above that we need to make
@(c) x ##1 @(d) y
match on two clock ticks, not three. I don't think this will be
confusing provided we explain that the clocking event controls themselves
do not account for any time advance, but rather determine to which clock
tick(s) the other sequence components advance.
Then in all cases where n > 0,
@(c) x ##n @(d) y
is legal and it matches on n+1 ticks with the following rule:
the first is a tick of c at which x must be true;
the next n-1 are ticks of c;
and the last is a tick of d at which y must be true.
It doesn't matter whether c and d are syntactically or semantically distinct.
The same rule applies always.
If we disallow
@(c) x ##1 @(d) y
and revert back to "##", which must be followed by an explicit clock,
then we are essentially killing the clock flow for sequences.
What do you think?
Best regards,
John H.
>
> --
> Dr. Bassam Tabbara
> Technical Manager, R&D
> Novas Software, Inc.
>
> http://www.novas.com
> (408) 467-7893
>
> > -----Original Message-----
> > From: John Havlicek [mailto:john.havlicek@motorola.com]
> > Sent: Monday, December 15, 2003 12:54 PM
> > To: bassam@novas.com
> > Cc: john.havlicek@motorola.com; sv-ac@eda.org
> > Subject: Re: [sv-ac] parsing problem
> >
> >
> > Hi Bassam:
> >
> > I understand the desire to have
> >
> > (1) @(c) s ##n @(d) t
> >
> > mean the same thing as
> >
> > (2) @(c) s ##n 1 ## @(d) t
> >
> > in 3.1, but I think there are undesirable consequences of doing
> > this.
> >
> > I think it will be very bad if we have to make the formal
> > semantics keep track of whether the clock is actually changed
> > or not. Keeping track means that the notion of "change",
> > even if not defined, must be introduced into the semantics
> > and the simple inductive structure of the definition will
> > have to be complicated by checks for clock change.
> >
> > Assuming that the semantics of ##n follows the same rule
> > whether or not the clock is actually changed, then I can
> > substitute d = c in (1) and (2) to get that
> >
> > (1') @(c) s ##n @(c) t
> >
> > means the same thing as
> >
> > (2') @(c) s ##n 1 ## @(c) t
> >
> > in 3.1, and it definitely does not mean the same thing as
> >
> > (2'') @(c) s ##n t
> >
> > in 3.1. What this says is that the @(c) really accounts for
> > 1 tick itself, whether or not the clock is changing.
> > Therefore, no clock event is redundant. They all involve
> > temporal advance.
> >
> > This is then at odds with the current clock resolution rules.
> > If I have
> >
> > sequence clocked_t;
> > @(c) t
> > endsequence
> >
> > sequence clocked_s_t;
> > @(c) s ##n clocked_t
> > endsequence
> >
> > then by the clock resolution rules, clocked_s_t is equivalent
> > to (2''). But by substitution, the user will expect
> > clocked_s_t to be equivalent to (1')
> >
> > I think that making (1) equivalent to (2) is also not good for
> > semantic alignment with PSL. In PSL,
> >
> > ((s)@c)@d
> >
> > is equivalent to
> >
> > (s)@c
> >
> > If SVA is aligned, we should have that
> >
> > @(d) @(c) s
> >
> > is equivalent to
> >
> > @(c) s
> >
> > But we will not have this, since no clock is redundant.
> >
> > If we reject the equivalence of (1) and (2) and solve the
> > problem by requiring a clock to be written after the "##",
> > then I think the restriction of a clock's scope by enclosing
> > parentheses will
> > have to be written in a funny way. Under the clock flow
> > proposal, you can write
> >
> > (3) @(c) s ## (@(d) t) ## u
> >
> > to mean the same thing as
> >
> > (4) @(c) s ## @(d) t ## @(c) u
> >
> > in 3.1. But with the rule that ## must be followed by a clock, (3)
> > would have to be rewritten as
> >
> > (3') @(c) s ## @(e) (@(d) t) ## @(c) u
> >
> > where e can be any clock. In other words, this rule means that the
> > clock flow across parentheses is useless.
> >
> > Comments?
> >
> > Best regards,
> >
> > John H.
> >
> >
> > >
> > > I never liked the bare "##" anyway.... However it does serve a
> > > *practical function* which is: a specific number is rather
> > confusing.
> > > If I were to go with a specific delay number there I would
> > rather it
> > > was 0 ... Essentially the thinking is that any delay refers to the
> > > *current* clock so "0" is more adequate. ##1 bugs me since
> > we really
> > > mean go to "earliest" different clock (from right now, not a cycle
> > > later...).
> > >
> > > See what I mean by: it serves a practical function ? :-)!
> > That said,
> > > what is the problem we are trying to solve again ? I would
> > rather we
> > > not make the "optional" bit in the clock flow (if someone uses the
> > > multi-clock concatenation they better switch the clock, if
> > they don't
> > > well they can put it again ... :-)!).
> > >
> > > -Bassam.
> > >
> > >
> > > --
> > > Dr. Bassam Tabbara
> > > Technical Manager, R&D
> > > Novas Software, Inc.
> > >
> > > http://www.novas.com
> > > (408) 467-7893
> > >
> > > > -----Original Message-----
> > > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On
> > Behalf Of
> > > > John Havlicek
> > > > Sent: Monday, December 15, 2003 7:15 AM
> > > > To: sv-ac@eda.org
> > > > Subject: [sv-ac] parsing problem
> > > >
> > > >
> > > > All:
> > > >
> > > > Surrendra has pointed out that my proposal 12 on clock flow
> > > > introduces a parsing problem. I am not well enough versed in
> > > > lexical analysis and parsing to give you a technical
> > > > characterization of the problem, but I will describe it.
> > > >
> > > > The proposal makes optional the specification of the
> > clock in places
> > > > that it is redundant. Thus, it is not necessary to write a clock
> > > > event after the multi-clock concatentation "##" if the clock does
> > > > not change. This makes it somewhat tricky to figure out whether
> > > > what follows "##" is a parameter expression for a "##n"
> > operator or
> > > > a sequence expression that is the right-hand operand of
> > "##". For
> > > > example
> > > >
> > > > @(c) s ## 2 ## 3 ## 4 ## 5 ## 6
> > > >
> > > > vs.
> > > >
> > > > @(c) s ## 2 ## 3 ## 4 ## 5 ## 6 7
> > > >
> > > > The latter actually means
> > > >
> > > > @(c) s ##2 ##3 ##4 ##5 ##6 7
> > > >
> > > > A simple solution is to change the multi-clock
> > concatenation symbol
> > > > so that it is not identical to the base operator symbol for the
> > > > parameterized concatenations "##n".
> > > >
> > > > Surrendra and I have discussed an alternative solution
> > that may be
> > > > better. The alternative is to get rid of the special symbol for
> > > > multi-clock concatenation and just use the parameterized "##n" in
> > > > both
> > > > singly- and multiply-clocked sequences. In the formal semantics,
> > > > "##" means the same thing as "##1", so to get the effect
> > of the old
> > > > "##" one would write "##1" instead.
> > > >
> > > > For example,
> > > >
> > > > OLD: @(c) s ## @(d) t
> > > >
> > > > NEW @(c) s ##1 @(d) t
> > > >
> > > > One could also use any "##n", n > 0, when changing the clock:
> > > >
> > > > OLD: @(c) ##(n-1) 1 ## @(d) t
> > > >
> > > > NEW: @(c) ##n @(d) t
> > > >
> > > > The intuition for "##n", n > 0, in any sequence, whether
> > singly- or
> > > > multiply-clocked, is then the following:
> > > >
> > > > s ##n t
> > > >
> > > > means that from the ending point of s, there are n clock tick
> > > > advances to get to the starting point of t. The first
> > n-1 of these
> > > > advances are to clock ticks of the ending clock of s,
> > while the last
> > > > advance is to a clock tick of the leading clock of t.
> > > >
> > > > Best regards,
> > > >
> > > > John H.
> > > >
> >
This archive was generated by hypermail 2b28 : Wed Dec 17 2003 - 08:25:15 PST