Subject: RE: [sv-ac] parsing problem
From: Surrendra Dudani (Surrendra.Dudani@synopsys.com)
Date: Tue Dec 16 2003 - 09:54:52 PST
Hi Bassam,
The line of reasoning is similar to the case of non-overlapping
implication. That is,
@(c1) s1 |=> @(c2) s2
For a match of s1, the implication operator advances the last tick of c1 to
the nearest tick of s2. If c1 and c2 are identical, then it is equivalent
to ##1. So, for a single match of s1, it is same as writing
@(c1) s1 ##1 @(c2) s2 // in the proposed syntax
regardless of whether c1 and c2 are identical.
##1 just says to advance to the next tick of whichever clock that follows.
Please note that merging ##0 effect is not allowed for implication
(overlapping implication) or for concatenation when the two clocks are
different.
Hope it clarifies some...
Surrendra
At 08:55 AM 12/16/2003 -0800, you wrote:
>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.
> > > >
> >
**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive, Suite 300
Marlboro, MA 01752
Tel: 508-263-8072
Fax: 508-263-8123
email: Surrendra.Dudani@synopsys.com
**********************************************
This archive was generated by hypermail 2b28 : Tue Dec 16 2003 - 09:55:31 PST