Subject: RE: [sv-ac] parsing problem
From: Bassam Tabbara (bassam@novas.com)
Date: Tue Dec 16 2003 - 08:55:03 PST
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.
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.
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.
-- 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 : Tue Dec 16 2003 - 08:55:45 PST