Subject: RE: [sv-ac] parsing problem
From: Bassam Tabbara (bassam@novas.com)
Date: Wed Dec 17 2003 - 10:45:00 PST
Hi John,
Thank -you- for the detailed explanation, sorry to put you through that,
but I think you clearly mentioned one issue which we *both* agree on:
"number of ticks". To make a long story short we really see eye-to-eye
on that, what I skipped is "accounting for the extra @c's vs. just
throwing them away .."
Consider the following:
> In 3.1, to match
>
> @(c) x ## @(d) y -now @c-
>
> there are two clock ticks:
>
> c d -c-
> x y
The issue that had bugged me is that is takes a ##1 to from one *c* to
the next in: c d c, so if I were to think of the "d", then (conceivably)
means that it is in the realm of a "##0" from the first c, and then I
started thinking from there (what if c and d were overlapped...).
** But yes we already (in 3.1, I see it now on p. 177, I reinvented that
in a different way, sorry ... ) say that @(c) s ## @(c) t means: @(c) s
##1 t (which is I think what Surrendra also pointed out in a different
way that the ##0 with two @c's is disallowed effectively), then my
thinking has no standing really (the question becomes what if d got
overlapped with the next c and we get the ##1).
Thanks John for the detailed explanation, I was indeed "optimizing" the
extra @(c)'s and not counting them, writeup below much appreciated.
Thx.
-Bassam.
-- 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: Wednesday, December 17, 2003 8:24 AM > To: bassam@novas.com > Cc: john.havlicek@motorola.com; sv-ac@eda.org > Subject: Re: [sv-ac] parsing problem > > > 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 - 10:45:54 PST