RE: [sv-ac] proposal for Mantis 1728

From: Korchemny, Dmitry <dmitry.korchemny_at_.....>
Date: Tue Aug 21 2007 - 06:48:44 PDT
Hi Shalom,

Please, see my comments below.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Bresticker, Shalom
Sent: Sunday, August 12, 2007 3:33 PM
To: john.havlicek@freescale.com; sv-ac@server.eda-stds.org
Subject: RE: [sv-ac] proposal for Mantis 1728

See my comments inside. I did not thoroughly study every word.

> -----Original Message-----
> From: owner-sv-ac@server.eda.org 
> [mailto:owner-sv-ac@server.eda.org] On Behalf Of John Havlicek
> Sent: Tuesday, August 07, 2007 5:39 PM
> To: sv-ac@server.eda-stds.org
> Subject: [sv-ac] proposal for Mantis 1728
> 
> Hi Folks:
> 
> I had an action item to look at the proposal for 1728 and, if 
> appropriate, call for a vote.
> 
> I have spent some time with the proposal, and my opinion is 
> that it's not ready for vote.  I've copied comments below.
> 
> I also think there are some basic questions about elaboration 
> raised by Gord that we should discuss.
> 
> If others disagree with my opinion about the state of the 
> proposal, then we can discuss that and consider proceeding, 
> on motion, with a vote.
> 
> J.H.
> 
> Notes 2007-08-06
> ----------------
> 

In the BNF on page 1, there should be white space between tokens.
For example, between let_identifier and the left bracket.

> p. 1.  I don't think it is appropriate to call such a thing a 
> "let statement".
>    We already have a notion of "statement" in the language, 
> and this construct
>    does not fit it.  An instance of a let declaration seems 
> to me to stand as
>    an expression, not as a statement.  I recommend that the 
> phrase "let statement"
>    be replaced throughout by something like "let expression". 
>  Also, I recommend
>    that the phrase "let definition" be replaced by "let 
> declaration" throughout.

I suggest 'let construct' in most of the places.

[Korchemny, Dmitry] Adopted

"The let statement provides means" ->
"The let construct provides a means"

In general, the proposal needs a proofreading for the English.

> 
> p. 1, LRM-ese:   
>    . that can be used in other let statements  --> 
>      that may be used in other let statements 
>    . may be used for customization and may replace the 
> compiler directives -->
>      can be used for customization and can replace the 
> compiler directives

"packages (25)" ->
"packages (See Clause 25)"

[Korchemny, Dmitry] Fixed
> 
> p. 2, LRM-ese:
>    . the let statement may serve this purpose  -->
>      the let statement can serve this purpose 
> 
> p. 2.  I recommend
>    . the let statement cannot be substituted by a function -->
>      the let expression cannot be replaced by a function call
> 
> p. 2. I don't think it is a good idea to put a statement like
> 
>       The only alternative to let is a compiler directive 
> with the disadvantages
>       as described earlier: ...
> 
>    in the LRM.  I recommend omitting this as a proposed 
> addition to the LRM
>    or rewriting the point so that it compares using let to 
> using a compiler
>    directive without claiming that there is no other alternative.

I agree.


> 
> p. 2. 
> 
>       A synthesis tool may treat the auxiliary signals such as c as
>       real ones and synthesize them into silicon. This may not be
>       desirable.
> 
>    I am hesitant about referencing synthesis in the LRM in 
> this way.

I agree.


>  The
>    following comment also applies to this text.
> 
> p. 2.  In general, I think that the rationalization or 
> defense of the existence
>    of "let" in this discussion is not appropropriate for the 
> LRM.  If the proposal
>    is passed and approved, then it will be a part of the 
> standard.  Instead, I think
>    this section should focus primarily on describing 
> capabilities, secondarily on 
>    comparisons with alternative capabilities, and avoid the 
> editorial commentary.
>    Examples can show advantages of using let without saying 
> that other mechanisms
>    are "awkward", "workarounds", etc.

It is appropriate to describe the uses and advantages of a certain
construct, but without disparaging other constructs. It is appropriate
to note that in certain contexts, a certain construct may have
advantages over a different construct. But the text should not imply
that, for example, let is better than `define, just that in certain
contexts, let may have certain advantages.

[Korchemny, Dmitry] Fixed

"Another use or let" ->
"Another use for let"

[Korchemny, Dmitry] Fixed

There should be more consistency in bolding of 'let'.

[Korchemny, Dmitry] Fixed

> p. 2.  "are two-bit wide" is an awkward phrase in English;  
> "are of bit width two"
>    or "are of two-bit width" are preferable.

You can say "are two bits wide".

"then c will also two-bit wide" ->
"then c will also be two bits wide"


> p. 2.  I recommend changing 
> 
>       The let statements can define parameterized expressions that can
>       be instantiated in sequences, properties, verification
>       statements and other let definitions.  Let cannot be
>       instantiated in action blocks of verification statements.
> 
>   to 
> 
>       A let declaration defines a template expression, parameterized
>       by its ports.  A let declaration may be instantiated in
>       sequences, properties, verification statements, and other let
>       declarations.  A let declaration shall not be instantiated in
>       the action block of a verification statement.

"verification statement" appears only twice in Draft 3a, both at the
beginning of 16.14. If you want to use the term here, you need a
cross-reference to that subclause.

[Korchemny, Dmitry] Fixed.

As a side note, if that term is to have a specialized, specific meaning,
it should be italicized in 16.14 and added to the Glossary as well.

[Korchemny, Dmitry] Opened a new Mantis item 1987

"SystemVerilog Assertions" ->
"SystemVerilog assertions"
The term appears 4 times in Draft 3a, all with 'assertions'
uncapitalized.

[Korchemny, Dmitry] Fixed and moved to the motivation section.

"The let statement is characterized as follows" - 
This is not consistent with the style of this LRM.
No other construct, I think, is described in this way.

[Korchemny, Dmitry] Fixed.

> p. 2.  
> 
>       The operand types are restricted the same way as in Boolean
>       expressions used in assertions (16.5.1).n
> 
>    "operand" of a let is not defined.  Operators have 
> operands, but let is
>    not an operator.  Something else is intended, and the 
> language should be made
>    clearer.

"Boolean" -> "boolean" (uncapitalized throughout the LRM)

[Korchemny, Dmitry] Fixed.

> 
> p. 2, LRM-ese:
>    . formal arguments can optionally be typed -->
>      formal arguments may optionally be typed
> 
> p. 2.  
> 
>        following the same syntactic form as for arguments to sequences
>        and properties (16.7.1)
> 
>    The BNF productions are not the same, so I am concerned 
> about the statement
>    that the syntactic form is the same as for arguments to 
> sequences and 
>    properties.  Does this comparison need to be made?
> 
> p. 2.  Check the green on the note to the editor:  I think 
> the parentheses 
>    should be green.

No matter.


> p. 2, LRM-ese:
>    . formal argument can have optional default values -->
>      formal argument may have optional default values
> 
> p. 2.
> 
>       Scoping rules are such that referenced identifiers / names in
>       the let expression which are not formal arguments bind in the
>       declarative scope of the let statement
> 
>    I recommend avoiding "identifiers/names" and similar slash 
> constructs.
>    I recommend looking at other places in the LRM where this 
> scoping concept
>    is discussed (22.8?) and emulating the turns of phrase 
> used in them.

Here 'identifiers' is sufficient.
Same elsewhere in the proposal.

[Korchemny, Dmitry] This section was rewritten. Not relevant anymore.

> pp. 2-3.  Why do globally referenced names in a let 
> declaration have to
>    be declared before used?  Similarly, why does a let construct have
>    to be declared before being instantiated?  Do these rules apply to
>    other declared items, like tasks, functions, sequences, or
>    properties?  It will be useful for discussion of this 
> proposal to get 
>    pointers to other places in the LRM that discuss this kind 
> of requirement.
>    There may be other places in Clause 16 that should be scrutinized. 
>    See also Mantis 1852.
> 
>    In 6.5, I found
> 
>       Data must be declared before they are used, apart from implicit
>       nets (see 6.9).
> 
>    From the context, I think "data" here refers only to nets 
> and variables.
> 
>    I have not found statements about the relationship of 
> calls to tasks
>    or functions and their declarations.

Tasks and functions are different in that if they are not declared
previous to the call, the call is considered a hierarchical reference,
and follows the rules of hierarchical references to tasks and functions.
That is, if module A instantiates module B, then B can contain a call to
a subroutine which is declared within A. That same mechanism enables the
compiler to find the subroutine if it is declared within B following the
call.

[Korchemny, Dmitry] See my answer to John.

> p. 3.
> 
>       The let expression is substituted in the place of instantiation
>       without any partial evaluation of the expression, the same way
>       as sequences do. The substituted expression is enclosed in
>       parentheses (...) so as to preserve the priority of evaluation
>       of the let expression. Recursive let instantiations are not
>       permitted.
> 
>    I think this paragraph should say somehow that it is describing the
>    meaning or semantics of a let instance.  I don't think the 
> comparison
>    to sequences is clear as a normative specification.  I 
> think it will
>    be better to write the description of the semantics as an 
> independent
>    statement, borrowing or emulating turns of phrase from 
> other parts of
>    the LRM.

Previous versions of this proposal used the term 'inlining'. But that
term is not used in the LRM except in a couple of places that are not
relevant here. So the comparison to sequences is used. 

[Korchemny, Dmitry] I am not using 'inlining' in the proposal

The reference to sequences is to the following text in 16.7: 
"The evaluation of a sequence that references a named sequence is
performed in the same way as if the named sequence was contained as a
lexical part of the referencing sequence, with the formal arguments of
the named sequence replaced by the actual ones and the remaining
variables in the named sequence resolved according to the
scope of the declaration of the named sequence."

That text could be more or less repeated here, replacing 'sequence' with
'let expression' and adapting the text as necessary to the context.

[Korchemny, Dmitry] Rewritten in a similar way.

> p. 3, LRM-ese:
>    . Let expressions can contain -->
>      A let expressions may contain -->

Generally, the use of 'can', 'may', 'must', 'shall', etc. should be
reviewed and should conform to IEEE style.

[Korchemny, Dmitry] Done.

"Their clock if not explicitly specified is inferred" ->
"Their clock, if not explicitly specified, is inferred"

[Korchemny, Dmitry] Fixed.

> p. 3.
> 
>       The let statement identifier must be unique in its namespace.
> 
>    Check whether let is covered by the rules in 22.6, which applies to
>    an entire SystemVerilog description.  Also see 22.8.

22.6 is clear: "A particular identifier can be declared at most once in
any scope."

[Korchemny, Dmitry] Therefore I think that this statement may be
dropped.

> p. 3.  I would remove the comparison to functions in talking 
> about importing from
>    a package.  I recommend changing 
> 
>       Like functions, let statements can be imported from a
>       package. 
> 
>    to
> 
>       A let declaration may be imported from a package.
> 
>    I don't understand the following:
> 
>       Binding of identifiers / names that are not formal arguments
>       must be satisfied by the declarations in the package.
> 
>    Is this a reiteration of the scoping condition from item 5 
> above, or is
>    it something new and different?  Again, avoid the slash 
> combinations.

Same as item 5.

[Korchemny, Dmitry] See my answer to John.

I did not time today to review the rest of John's comments.

Shalom


> p. 3.  I think the phrase "after substitution of let 
> definitions" is awkward.
>    It will be good to find a better phrase for this, such as 
> "replacement of
>    let instances" and try to make the meaning of this phrase 
> clear in item 7
>    on let semantics.  This phrase should be used consistently 
> throughout the
>    presentation of the examples.
> 
> p. 3.  There is a missing ")" in the a1 assertion in two 
> places in example 1.
> 
> p. 3.  I found surprising the appearance of the hierarchical 
> paths, such as "m.p", 
>    in the second version of m in example 1.  Are they needed 
> in this example?  
>    Is the point to avoid any issues with the order of 
> declaration and reference?
> 
> p. 4.  In example 3, the sequence declaration in the second 
> module top that 
>    is commented out is confusing.  Why is this declaration 
> any different than
>    the code in the first module top?  The declaration is 
> misleading because
>    "x" changes to "top.a".
> 
>    Also, why is this example showing elaboration of both the 
> let instance 
>    and the sequence instance?  Is this related to Gord's 
> criticism that this
>    proposal, and the assertion Clause, assume an elaboration 
> algorithm that
>    does not exist?
> 
>    Semantically, does elaboration of let instances commute 
> with elaboration
>    of sequence and property instances?  Can the elaboration 
> of let instances
>    that appear within sequences or properties be incorporated 
> into the rewriting 
>    algorithm of 1549?
> 
> p. 5.  In example 5, second module m, can the outer begin 
> block labels 
>    use the constant expressions in square brackets, like 
> "L0[0]"?  From 
>    the syntax, I think these have to parse as block_identifier, which 
>    must parse as identifier.
> 
> p. 5.
> 
>       Note that the let statements may not be referred to
>       hierarchically using the paths m.L0[0].L1 and m.L0[2].L1.
> 
>    I assume that this means "let declarations", not "let 
> statements", and 
>    I wonder why is this so?  I don't recall this being 
> specified before, so
>    this seems like a normative note.  More generally, why 
> should this be so?
> 
> p. 6.
> 
>       However, if the function or the variable were referred to
>       directly in the code, it would have to be imported explicitly.
>    
>    I don't understand this.  What code is being referred to?  
> My intuition
>    is that this example is trying to illustrate a general 
> restriction of
>    importation that probably is not necessary.
> 
> pp. 6-7.  Similar remarks to previous ones about elaborating. 
>  My reaction
>    is that the example goes beyond the concepts of "let" and 
> is re-illustrating
>    other concepts.  
> 
>    In general, my sense is that either the number of examples 
> could be reduced
>    by combining some of the concepts or the complexity of the 
> individual 
>    examples could be reduced by focussing each one.
> 
> p. 13.  Why is "operator_assignment" stricken from the 
> sequence_match_item 
>    production?  What is the technical consequence of this?

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Tue Aug 21 06:50:17 2007

This archive was generated by hypermail 2.1.8 : Tue Aug 21 2007 - 06:50:31 PDT