Thanks Dimitry. One more thing I noticed is different from sequence/property declaration is the formal declarations for let. In your proposal you have: let_port_list ::= let_port_item {, let_port_item} let_port_item ::= { attribute_instance } let_formal_type identifier [= expression] Whereas for properties/sequences we have (I think it is similar for functions/tasks): sequence_port_list ::= sequence_port_item {, sequence_port_item} sequence_port_item ::= { attribute_instance } sequence_formal_type port_identifier {variable_dimension} [ = expression ] So, the {variable_dimension} is missing for let. Is it intended or it was just an oversight. Manisha -----Original Message----- From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: Thursday, September 20, 2007 8:21 PM To: Kulshrestha, Manisha; sv-ac@server.eda-stds.org Subject: RE: [sv-ac] call to vote on 1728 Hi Manisha, I updated the proposal according to your comments. Thanks, Dmitry -----Original Message----- From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Kulshrestha, Manisha Sent: Wednesday, September 19, 2007 7:48 PM To: sv-ac@server.eda-stds.org Subject: RE: [sv-ac] call to vote on 1728 Hi Dimitry, The proposal looks fine now. Here are some minor editorial changes I would recommend for the proposal as some places usage of declaration and expression words is mixed up: On page 3: Furthermore, including let statements into packages (see Clause 25) ... Should be Furthermore, including let declarations into packages (see Clause 25) ... On page 4: Like in sequences and properties, variables used in a let expression that are not formal arguments to the expression are resolved according to the scoping rules from the scope in which the let is declared. Should be: Like in sequences and properties, variables used in a let that are not formal arguments to the let are resolved according to the scoping rules from the scope in which the let is declared. This is more in line with a current statement like: Variables used in a sequence that are not formal arguments to the sequence are resolved according to the scoping rules from the scope in which the sequence is declared. On page 4: When a let expression is instantiated, actual arguments can be passed to the expression. Should be: When a let is instantiated, actual arguments can be passed to the let expression. Thanks. Manisha -----Original Message----- From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: Tuesday, September 18, 2007 2:51 PM To: Kulshrestha, Manisha; john.havlicek@freescale.com; eduard.cerny@synopsys.com; Seligman, Erik; bassam.tabbara@synopsys.com; Bustan, Doron; piper@cadence.com Cc: sv-ac@server.eda-stds.org Subject: RE: [sv-ac] call to vote on 1728 Hi Manisha, Please, see my comments below. I also found a redundant line in example c) remained from some older version: parameter int p = 0; and deleted it. Thanks, Dmitry -----Original Message----- From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com] Sent: Monday, September 17, 2007 7:51 PM To: Kulshrestha, Manisha; john.havlicek@freescale.com; Korchemny, Dmitry; eduard.cerny@synopsys.com; Seligman, Erik; bassam.tabbara@synopsys.com; Bustan, Doron; piper@cadence.com Cc: sv-ac@server.eda-stds.org Subject: RE: [sv-ac] call to vote on 1728 Hi, I have some more comments: 1. On page 3, it says "Another intended use of let is in modeling for assertions to provide shortcuts for identifiers or subexpressions.", I understand the usage for subexpressions but why would someone use a let construct for identifier ? [Korchemny, Dmitry] To provide a short name for a hierarchical identifier. Validators sometimes write their code in a separate module, and assertions in this module may reference signals from many different modules. Consider the following use case: let address1 = memory_claster.unitA.block2.addr1; let address2 = memory_claster.unitB.block1.addr2; a1: assert property (address1 != address2 |=> address1 == address2); 2. On page 3, "A let declaration may be instantiated in expressions of immediate assertions and match items of sequences, properties, verification statements, and other let declarations." In this statement, the ordering of words should be changed as match items apply to sequences and properties only. [Korchemny, Dmitry] I deleted the whole fragment. It is not relevant anymore. 3. On page 3, it says "The argument types are restricted the same way as in boolean expressions used in assertions (see 16.5.1)." Why are we putting same restrictions for let. Since let is going to get used in immediate asserts also it should not have any restriction on its declarations. Instead the checking should be done at the time of instantiation if the usage is correct or not. [Korchemny, Dmitry] If we do not limit let to boolean expressions only, there may be problems with the type inference, as pointed by Gord. I agree with you that this limitation can be relaxed, but it will require much more comprehensive proposal, involving tight interaction between different committees. Therefore we chose to begin with a reasonably limited version of the let proposal useful for assertions. The definition was designed in a way to allow future extensions without breaking the backward compatibility. I suggest we open a new Mantis item for relaxing the limitation you mentioned. 4. On page 4, " The let expression gets expanded with the actual arguments by replacing the formal arguments with the actual arguments." I think there should be some mention about typed formal arguments as this is not going to be entirely true in case of typed arguments as type casting will also be done along with replacement. [Korchemny, Dmitry] The above formulation is consistent to what is defined for sequences and properties in the LRM (see 16.7 for example). The explanation you are talking about is a subject of 1549 which hasn't been approved yet. When 1549 is approved the appropriate reference will need to be inserted. 5. On page 4, "let expressions may contain sampled value function calls (see 16.8.3). Their clock, if not explicitly specified, is inferred in the instantiation context in the same way as if the functions were used directly in sequences, properties or verification statements." I think this statement is ignoring the fact that let can be used outside of concurrent assertions also i.e. in immediate asserts. It should be mentioned that in case the usage is in immediate asserts, a clock must be specified (except for $sampled which does not require clock anymore based on some other proposals). [Korchemny, Dmitry] I rewrote it as: " let expressions may contain sampled value function calls (see 16.8.3). Their clock, if not explicitly specified, is inferred in the instantiation context in the same way as if the functions were used directly in the instantiation context. It shall be an error, if the clock is required, but cannot be inferred in the instantiation context." and added example f) to illustrate this point. 6. I would like to see an example of a concurrent assertion which uses typed arguments in the property declaration and also typed arguments to the let construct used in the property. I think it will be nice to show to the user that in this case actual will get type casted twice (once due to property's argument type and once again due to let's argument type). [Korchemny, Dmitry] I modified example e). Thanks. Manisha -----Original Message----- From: Kulshrestha, Manisha Sent: Monday, September 17, 2007 5:09 PM To: sv-ac@server.eda-stds.org Subject: RE: [sv-ac] call to vote on 1728 Hi, I vote no on the proposal. I noticed few corrections required in the proposal: 1. On page 3, In the footnote for let_instance (40) it says: "let_instance may be used only in the expressions which are part of sequence or property expressions, let declarations or immediate assertions." Whereas on the same page later it says: "A let declaration may be instantiated in other let declarations, sequences, properties, concurrent and immediate assertions." In the note (40), concurrent assertions are missing. On page (4) again it says "A let declaration may be instantiated in expressions of immediate assertions and match items of sequences, properties, verification statements, and other let declarations." This statement is again inconsistent with other such statements. What is the intended usage in match items ? Will it be used on the right hand side of assignment or it can also be used in arguments of the subroutine calls ? 2. The proposal does not say that let instance can be used in expect statement (expect statement is not included in concurrent assertions). Is that intended ? I think expect should be included in here. I am still looking at the proposal and send more feedback if I find any more issues. Thanks. Manisha -----Original Message----- From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of John Havlicek Sent: Wednesday, September 12, 2007 11:05 PM To: sv-ac@server.eda-stds.org Subject: [sv-ac] call to vote on 1728 Hi Folks: This is the call to vote on the proposal for Mantis 1728. The document is LetConstruct1728\ 070911_dk.pdf on Mantis. Please vote if you are eligible. See the details below. J.H. ------------------------------------------------------------------------ ------ Ballot on Mantis 1728 - Called on 2007-09-12, final ballots due at 2007-09-19 T 23:59-07:00 (PDT). v[xxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel) v[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys) n[-------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys) v[-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale) t[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair) v[xxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair) v[-xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor Graphics) n[---------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics) n[-------x--xxx.....................] Joseph Lu (Altera) v[xxxx..............................] Johan Martensson (Jasper) n[------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale) v[xxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence) v[xxxxxx-x-xxxxx-x..................] Erik Seligman (Intel) n[--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics) v[--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys) v[xxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems) |---------------------------------- attendance on 2007-09-11 |------------------------------------ voting eligibility for this ballot |------------------------------------- email ballots received Legend: x = attended - = missed r = represented . = not yet a member v = valid voter (2 out of last 3 or 3/4 overall) n = not valid voter t = chair eligible to vote only to make or break a tie -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean. --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean. --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Thu Sep 20 23:10:13 2007
This archive was generated by hypermail 2.1.8 : Thu Sep 20 2007 - 23:10:41 PDT