Hi Shalom, Please, see my notes below. Thanks, Dmitry ________________________________ From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Bresticker, Shalom Sent: Sunday, January 27, 2008 6:41 PM To: sv-ac@server.eda.org Cc: sv-champions@server.eda.org Subject: [sv-ac] Mantis 1900 comments - Part 1 Comments on Mantis 1900: - The Objectives section says, "Modules are always assumed to contain design code that is synthesizable into silicon". This is only an introduction to the proposal, but 'always' is not correct. How about 'often'? [Korchemny, Dmitry] Fixed. - In 16.3.6, "persists through the Observe region" should be "Observed region". [Korchemny, Dmitry] Fixed. - "It shall be considered an error if this method is used in disable iff boolean expression for properties." Add "the" before "disable iff". [Korchemny, Dmitry] Fixed. - In 16.3.6, "The value of method triggered evaluates to true if the given sequence has reached its end point at that particular point in time and false otherwise. The triggered status of the sequence is set in the Observed region and persists through the remainder of the time step. This method shall only be used in wait statements or boolean expressions (see 9.4.4) outside of sequence context". I know that this did not change in this proposal (except for one word), but since the proposal is already changing the paragraph, I think the cross-reference to 9.4.4 should be 9.4.5, and "sequence context" should be "a sequence context" or "sequence contexts". [Korchemny, Dmitry] Fixed. - "A sequence treats its formal argument as a local variable if the formal argument is used as an lvalue in operator_assignment or inc_or_dec_expression in sequence_match_item. " I would add helper words: "A sequence treats its formal argument as a local variable if the formal argument is used as an lvalue in an operator_assignment or inc_or_dec_expression in a sequence_match_item. " [Korchemny, Dmitry] Fixed. - 16.18.1 says, "Checker variables differ from regular variables in that they may be both deterministic and nondeterministic. They may have undefined or partially constrained values, while regular variables are always deterministic in the sense that they contain only one specific value at a time." I have not yet finished the proposal, but what does 'undefined' mean here? It seems a little strange. [Korchemny, Dmitry] "Undefined" means that the variable may contain any value of its type, and in formal verification when this variable is used in an assertion, this assertion is checked for all possible values of this variable. This is explained in 16.8.6: "A free variable may assume any value at every point in time, similarly to an input of the design. Formal analysis tools shall take into account all possible values of the free variables imposed by the assumptions and assignments (see 16.18.6.1). Simulators shall assign arbitrary values to the free variables consistent with the assumptions and the assignments." - "non-blocking" should be without hyphens, several times. [Korchemny, Dmitry] Fixed. - "The checkers may contain concurrent assertions, checker variable declarations and assignments, structural procedures," should be "structured procedures". [Korchemny, Dmitry] Fixed. - 16.8.1 has "The checkers may contain concurrent assertions, checker variable declarations and assignments, structural procedures, function declarations, let declarations, sequences and properties, and generate regions." There is another list on p. 11 in 16.8.2, starting with "A checker body may contain the following elements:". The lists are not identical, which is confusing. Better would be to have only one list. Duplication is a source of inconsistency. [Korchemny, Dmitry] I deleted the lists describing checker declaration and checker instantiation from 16.18.1 and left them only in 16.18.2 and 16.18.3. - Re "The following procedures are allowed in a checker (see 16.18.5): initial_check procedure, encapsulating assertions monitored on the first clock tick (similar to 16.14.5)". Here is a side issue. 16.14.5 says, "If the statement appears in an always procedure, the property is always monitored. If the statement appears in an initial procedure, then the monitoring is performed only on the first clock tick. Two inferences are made from the procedural context: the clock from the event control of an always procedure and the enabling conditions. A clock is inferred if the statement is placed in an always or initial procedure with an event control abiding by the following rules:' It is confusing that the second paragraph does not mention initial procedures. [Korchemny, Dmitry] Fixed. - 16.8.1 has "The checkers may be instantiated where concurrent assertions may be specified (see 16.14)," followed by a list. The list is not identical to 16.14's. 'A generate block' does not appear there. (I would just as soon delete the references to generate blocks, despite Gord's comment a few months ago). 16.18.3 has yet another list, "Checkers may be instantiated inside modules, programs, interfaces, and other checkers". [Korchemny, Dmitry] I deleted this list from 16.18.1, see above. I also removed a reference to concurrent assertions. - The proposal adds the keywords checker and endchecker. endchecker needs to be added to the list of endxxx keywords created in Mantis 1354. [Korchemny, Dmitry] Fixed. - BNF: Syntax 9-1 shows this: initial_keyword ::= initial | initial_check4 always_keyword ::= always | always_comb | always_latch | always_ff | always_check4 4) It shall be illegal to specify always_check or initial_check outside of a checker body. whereas the Syntax in 16.18.2 shows this: initial_keyword ::= initial2 | initial_check2 always_keyword ::= always2 | always_comb2 | always_latch2 | always_ff2 | always_check2 2. initial, always, always_comb, always_latch, and always_ff shall be illegal in a checker body. initial_check and always_check shall be illegal outside of a checker body. They have to be the same. I would do it this way: initial_keyword2 ::= initial | initial_check always_keyword2 ::= always | always_comb | always_latch | always_ff | always_check 2. initial, always, always_comb, always_latch, and always_ff shall be illegal in a checker body. initial_check and always_check shall be illegal outside of a checker body. Note that I put the footnote reference on the LHS of the production. [Korchemny, Dmitry] Fixed. Enough for one day. Regards, Shalom Shalom Bresticker Intel Jerusalem LAD DA +972 2 589-6582 +972 54 721-1033 -- This message has been scanned for viruses and dangerous content by MailScanner <http://www.mailscanner.info/> , 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 Jan 29 03:50:45 2008
This archive was generated by hypermail 2.1.8 : Tue Jan 29 2008 - 03:51:19 PST