Hi all, I am attaching a new version of let proposal. I haven't revised the VPI section, and it should probably be edited as well. Please, see my answers to John below. I will send my answers to Shalom in a separate mail. Thanks, Dmitry -----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. [Korchemny, Dmitry] I will send a separate mail regarding Gord's mail. 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 ---------------- 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. [Korchemny, Dmitry] OK. See also Shalom's comments. 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 [Korchemny, Dmitry] Fixed p. 2, LRM-ese: . the let statement may serve this purpose --> the let statement can serve this purpose [Korchemny, Dmitry] Fixed p. 2. I recommend . the let statement cannot be substituted by a function --> the let expression cannot be replaced by a function call [Korchemny, Dmitry] Fixed 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. [Korchemny, Dmitry] Moved to the motivation section. 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. The following comment also applies to this text. [Korchemny, Dmitry] Same comment. 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. [Korchemny, Dmitry] Same comment. 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. [Korchemny, Dmitry] Fixed 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. [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. [Korchemny, Dmitry] Fixed. p. 2, LRM-ese: . formal arguments can optionally be typed --> formal arguments may optionally be typed [Korchemny, Dmitry] Fixed. 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? [Korchemny, Dmitry] Changed to "similar". p. 2. Check the green on the note to the editor: I think the parentheses should be green. [Korchemny, Dmitry] Fixed. p. 2, LRM-ese: . formal argument can have optional default values --> formal argument may have optional default values [Korchemny, Dmitry] Fixed. 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. [Korchemny, Dmitry] Fixed. 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. [Korchemny, Dmitry] It looks like that LRM implicitly states that the there is no requirement for sequences and properties to be declared before being instantiated. For properties I deduce this from the fact that the mutually recursive properties are allowed, for sequences - from the fact that "Any form of syntactic cyclic dependency of the sequence names is disallowed" and the example on page 316 of the LRM. On the other hand as Shalom mentioned in his mail "Tasks and functions ... 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." Thus, the same situation should be true for sequences and properties: if a sequence is used before defined, it is actually an XMR. Since we do not allow XMR for let (as a result from our discussions with Gord), we should not allow using let constructs before their definition. Note also that the requirement of defining let before use implies that the there cannot be a cyclic dependency between let statements, therefore I am removing the latter requirement. As for the forward referencing the global names, it should be illegal according to (6.5), and therefore should not be explicitly stated here. 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. [Korchemny, Dmitry] Fixed. p. 3, LRM-ese: . Let expressions can contain --> A let expressions may contain --> [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. [Korchemny, Dmitry] See my answer to Shalom. 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. [Korchemny, Dmitry] I think it is sufficient to mention the scopes let may be declared (as they are mentioned for sequences and properties). Therefore I am dropping all the rest. 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. [Korchemny, Dmitry] Using the phrase " The effective code after expanding let instances" now. p. 3. There is a missing ")" in the a1 assertion in two places in example 1. [Korchemny, Dmitry] Fixed. 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? [Korchemny, Dmitry] The hierarchical references are used to stress the scope. 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? [Korchemny, Dmitry] I left instance unexpanded and deleted the rest of the example. Thus, example 4 becomes redundant and I am deleting it. 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? [Korchemny, Dmitry] This is the same elaboration mechanism. 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. [Korchemny, Dmitry] Yes, this syntax is illegal, and I don't see any simple way to express the expansion in the code. Therefore I am using English prose to describe the resulting expansion. 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? [Korchemny, Dmitry] Hierarchical reference is an XMR, and let XMR are forbidden. Actually, the reason why XMR is forbidden lies in hierarchical references to let declarations in generate statements. Consider the following example provided by Gord: Is the following legal: for (genvar i = 0; i < 5; i++) begin : b if (i < 4) begin:c let x = b[i+1].c.x end else begin:c let x = 0; end end Does iteration i+1 "exist" at the time iteration i has its "let" defined? Upon rethinking, I don't see a big issue here, but it becomes difficult to define how to open let statement in a general case. Therefore we decided not to allow let XMR. This limitation may be always removed in the future. 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. [Korchemny, Dmitry] See the next comment. 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 focusing each one. [Korchemny, Dmitry] I agree. Removing the redundant examples. p. 13. Why is "operator_assignment" stricken from the sequence_match_item production? What is the technical consequence of this? [Korchemny, Dmitry] The reason was to replace it with local_var_assignment which would contain let expression in sequences. It looks to me that a better way to incorporate a let expression into the grammar is to make it a special kind of expression and add to add a note limiting let instantiation by properties, sequences, assertions etc. only. Note also that the item concurrent_assertion_item_declaration becomes problematic, since it may now be a let_statement, and the let statement may be used in immediate assertions as well. Therefore I am renaming it to assertion_item_declaration. -- 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.
This archive was generated by hypermail 2.1.8 : Tue Aug 21 2007 - 06:45:08 PDT