Subject: RE: [sv-ac] errata, JH group 1
From: Bassam Tabbara (bassam@novas.com)
Date: Wed Jan 21 2004 - 10:28:03 PST
John,
I skimmed through this and it looks good. I think based on the discussion we
had last time, is it reasonable to add an "example" (say in > 5. 17.11.1,
p. 245. Change), and may be even some words earlier in the text (although I
think the wording already makes this clear in:
">The single delay
> indicated by ##1 is understood to be from the endpoint of the
> first sequence, which occurs at a tick of the first clock, to
> the nearest strictly subsequent tick of the second clock, where
> the second sequence begins."
to the effect that "##0" is not allowed (semantically, since the BNF admits
that...).
May be just an example is ok ... I do not think this is -that- obvious,
better to make it clear.
Thx.
-Bassam.
-- Dr. Bassam Tabbara Technical Manager, R&D Novas Software, Inc.http://www.novas.com (408) 467-7893
> -----Original Message----- > From: owner-sv-ac@server.eda.org > [mailto:owner-sv-ac@server.eda.org] On Behalf Of John Havlicek > Sent: Tuesday, January 20, 2004 11:01 PM > To: sv-ac@server.eda.org > Cc: dwsmith@synopsys.com > Subject: [sv-ac] errata, JH group 1 > > > All: > > Below is a group of two errata for SVA 3.1a Draft 3. > > The first is the most important. It is the parsing problem > that results from the special "##" multi-clocked > concatenation under clock flow. There was discussion in > December about solving this problem by getting rid of the > special "##" and simply allowing general concatenations for > multi-clocked sequences. I have decided not to propose this > solution for two reasons: > > > 1. It involves substantial changes to the LRM. > > 2. It leaves a semantic glitch with the interaction of general > multi-clock concatenations and clock flow. To see this, > consider > > @(c) (x ##1 @(d) y) ##3 z > > Clock flow says this should mean the same as > > @(c) x ##1 @(d) y ##3 @(c) z > > and we said in December that this should mean the same as > > @(c) x ##1 @(d) y ##2 1 ##1 @(c) z > > But then we have the effect that the clock @(d) has flowed out of > its enclosing parentheses onto the first two ticks of the ##3. > This "leakage" of @(d) out of the parentheses is unacceptable in my > opinion because it means that > > @(c) (x ##1 @(d) y) ##3 z > > is not equivalent to > > @(c) (x ##1 @(d) y) ##1 1 ##2 z. > > > I have therefore chosen to propose a much more modest > solution. It is simply that we replace the special "##" with > "##1". This solution eliminates the parsing issue because > every "##" must now be followed by a parameter. It > eliminates the semantic glitch because "##1" does not admit > alternative decompositions that can lead to different results > under clock flow. > > In the formal semantics, "##" already means the same thing as > "##1", so this is the most natural choice in my opinion. > > [Note that the only reason the same parsing problem did not > exist in 3.1 is that the special "##" had to be followed by > "@". In other words the special "##" was really like "##@(c)".] > > Best regards, > > John H. > > ============================================================== > ================== > > SVA 3.1A DRAFT 3 ERRATA, JH GROUP 1 > > ============================================================== > ================== > Erratum JH1: Parsing Problem with Clock Flow > ============================================================== > ================== > > Discussion > ---------- > > Proposal 12 on Clock Flow 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 > introduces a parsing problem in determining whether what > follows "##" is the parameter "n" of a singly-clocked "##n" > or an expression operand of a multiply-clocked "##". The > difficulty is illustrated in in the following 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 > > > The proposed solution is to use "##1" instead of the special > symbol "##" for multi-clock concatenation. In the formal > semantics, "##" already means the same thing as "##1". This > solves the parsing problem because every "##" must be > followed by a parameter. "##1" is the only concatenation > operator allowed for joining differently clocked sequences. > > The BNF for multi_clock_sequence allows a general > cycle_delay_range for combining two multiply-clocked > sequences. The semantic restriction > to "##1" is described in the LRM text. > > > BNF Changes > ----------- > > 1. 17.6, Syntax Box 17-4. Change > > multi_clock_sequence ## multi_clock_sequence > > to > > multi_clock_sequence cycle_delay_range multi_clock_sequence > > 2. 17.11, Syntax Box 17-15. Change > > multi_clock_sequence ## multi_clock_sequence > > to > > multi_clock_sequence cycle_delay_range multi_clock_sequence > > 3. Annex A, p. 410. Change > > multi_clock_sequence ## multi_clock_sequence > > to > > multi_clock_sequence cycle_delay_range multi_clock_sequence > > > LRM Text Changes > ---------------- > > 1. 17.11.1, p. 245. Change the first paragraph from > > Multiply-clocked sequences are built by concatenating > singly-clocked subsequences using the multi-clock concatenation > operator ##. This operator is non-overlapping and synchronizes > between the ending clock tick of the left hand sequence and the > strictly subsequent starting clock tick of the right hand > sequence. > > to > > Multiply-clocked sequences are built by concatenating > singly-clocked sequences using the single-delay concatenation > operator ##1. This operator is non-overlapping and synchronizes > between the clocks of the two sequences. The single delay > indicated by ##1 is understood to be from the endpoint of the > first sequence, which occurs at a tick of the first clock, to > the nearest strictly subsequent tick of the second clock, where > the second sequence begins. > > 2. 17.11.1, line 9, p. 245. Change > > the above sequence is equivalent to > > to > > the above sequence is equivalent to the singly-clocked sequence > > > 3. 17.11.1, p. 245. Change > > When using the multi-clock concatenation operator ##, both > operands are required to admit only non-empty matches. > > to > > When concatenating differently-clocked sequences, the maximal > singly-clocked subsequences are required to admit only non-empty > matches. > > > 4. 17.11.1, p. 245. Change > > The restriction to operands that do not match the empty word > when using ## ensures that any multiply-clocked sequence has > well-defined starting and ending clocking events and > well-defined clock changes. > > to > > The restriction that maximal singly-clocked subsequences not > match the empty word ensures that any multiply-clocked sequence > has well-defined starting and ending clocking events and > well-defined clock changes. > > 5. 17.11.1, p. 245. Change > > Differently-clocked or multiply-clocked sequence operands cannot > be combined with any sequence operators other than the > multi-clock concatenation operator ##. For example, the > following is illegal: > > (@(posedge clk1) x ##1 y) intersect (@(posedge clk2) z[*1:$]) > > to > > Differently-clocked or multiply-clocked sequence operands cannot > be combined with any sequence operators other than ##1. > For example, if clk1 and clk2 are not identical, then > the following > are illegal: > > (@(posedge clk1) x ##1 y) intersect (@(posedge clk2) z[*1:$]) > > (@(posedge clk1) s1) ##2 (@(posedge clk2) s2) > > 6. 17.11.1, p. 245. Change all remaining instances of "##" to "##1" > (but do not change "##1" to "##11"). [7 instances] > [Note: There are 11 instances of "##" in this section in Draft 3, > but 4 of these should be eliminated by the preceding changes.] > > 7. 17.11.2, p. 246. Examples on p. 246, change "##" to "##1" > (but do not change "##1" to "##11"). [3 instance] > > > 8. 17.11.3, p. 247. Examples on p. 247, change "##" to "##1" > (but do not change "##1" to "##11"). [8 instances] > > > 9. 17.11.3, p. 248. Examples on p. 248, change "##" to "##1" > (but do not change "##1" to "##11"). [10 instances] > > > Formal Semantics Changes > ------------------------ > > 1. H.2.1, p. 484. In the abstract grammar for clocked > sequences, change "##" > to "##1". > > 2. H.2.3.1, second bullet, p. 485. Change "##" to "##1". > > 3. H.3.1, p. 487. Delete the bullet "(S_1 ## S_2) |---> (S_1 > ##1 S_2)". > > > > ============================================================== > ================== > Erratum JH2: Clocked sequence parenthesis form missing in > formal semantics > ============================================================== > ================== > > Discussion > ---------- > > By oversight, the BNF change allowing parentheses to be used > on multiply-clocked sequences was not paralleled in the > formal semantics. > > Formal Semantics Changes > ------------------------ > > 1. H.2.1, p. 484. Add a production to the abstract grammar > for clocked > sequences. Change > > S ::= @(b) R // "clock" form > | ( S ## S ) // "concatenation" form > > to > > S ::= @(b) R // "clock" form > | ( S ) // "parenthesis" form > | ( S ##1 S ) // "concatenation" form >
This archive was generated by hypermail 2b28 : Wed Jan 21 2004 - 10:35:05 PST