17.1 Introduction, first paragraph - "... to specify assertions (or properties) ..." Q: are assertions a specific form of properties or is 'assertions' and 'properties' interchangeable within this text? CHANGE: text "(or properties)" deleted. - I think it should say "There are two kinds of assertions: concurrent _and_ immediate.", but I am not a native english speaker ... CHANGE: word "or" changed to "and" 17.1 Introduction, third paragraph - Q: Is it really required to mix 'clock semantics' and 'cycle-based semantics' to the extent this is done in this paragraph? RESPONSE: To the extent that this is an introductory section, it is ok. No Change 17.2 Syntax - Either there is a separate section for the syntax, which should contain _both_ syntax forms (immediate _and_ concurrent assertions) or this information is to be distributed to sections 17.3 and 17.4, like it is done for 17.3. We should be consistent here ... CHANGE: Some more description is added to descibe the top level view of assertions. - procedual_assertion_items is missing a 'r', it should say procedural_assertion_items CHANGE: procedual changed to Procedural - Q: I am unsure whether this BNF is correct? There is no disclaimer in this box, but Stephens BNF looks different and shows that everything derives from procedural_assertion_items - In general I agree to the Editor's Note. CHANGE: This will be fixed in the final BNF 17.3 Immediate assertions, first paragraph - "The expression is treated as a condition like ??? in an if statement". Think there is something missing here... RESPONSE: The sentence now read: "The expression is non-temporal and treated as a condition as in an if statement. " - There is no mention of the action_block at all. A reader asks her/himself why? CHANGE: A sentence added: "The action_block specifies what actions are taken upon success or failure of the assertion" 17.3 Immediate assertions, BNF & second paragraph - Q: This paragraph describes basically the processing of the action block associated with the assertion. Why is this not mentioned? RESPONSE: Change as stated in the previous question - Either the BNF is wrong or the description is wrong, the description says the pass statement is optional as well; so my assumption is that the action_block is optional -- the square bracket around this are missing in the BNF IMHO. Stephen's BNF says statement_or_null for both statements, which would make both statements optional. Result is that 'assert(expr) else' is legal. Is this intended? RESPONSE: No, 'assert(expr) else ;' is legal. Statement_or_null takes care of teh semicolon. No Change - It would be beneficial to make clear when introducing the pass statement that this is the first statement within the action block, otherwise it is hard to tell which one is meant -- you need to read the whole paragraph to understand this. CHANGE: A sentence added: "The statement associated with the success of the assert statement is the first statement" - Is there a default behavior associated with an omitted (else) statement??? What happens in case of assert (expr) without anything? This is especially confusing since two paragraphs later it is stated "By default, the severity of an assertion failure is "error"". The final description here is stated nearly one page later at the beginning of the next page. Hmmm. CHANGE: The statement moved up: "If an assertion fails and no else clause is specified, the tool shall, by default, call $error, unless a tool-specific command-line option is enabled to suppress the failure." - The optional assertion label is not related to the action block. I would move this to a separate paragraph CHANGE: Created a new paragraph 17.3 Immediate assertions, third paragraph - This sounds like a failure of an assertion does result in an "$error" action, what is this default severity when there is no $fatal(), $error() system tasks defined at all. Does a simple assignment have a severity level ? Assume no, but this might be worth a footnote in the example at the end of this subsection. RESPONSE: Not sure what is meant by this question, System tasks are always defined. - It also states that the severity level of an assertion can be modified in the fail statement, what about the pass statement ??? RESPONSE: The usage of these system tasks in pass statements is not defined. 17.3 Immediate assertions, end of page 161 - What happens in case of more than one of these system tasks with conflicting severity (e.g. $fatal() followed by $info())??? Highest severity wins ? or last severity specified ? RESPONSE: All of them are executed, unless $fatal is included. Beginning of page 163 - should say "An assertion expression is always tied ..." CHANGE: Sentence changed to "An expression used in an assertion is always tied to a clock definition." Section 17.4 - does not describe concurrent assertions (with subsection what this is). Instead it identifies the variable value sampling (which is of course very important) and starts to define sequence expressionss at the end of this subsection. This is confusing. - when sequences are a part of concurrent assertions then this should be subsections. Or 17.4 should give some overview how the subsections 17.5 - ??? are related to concurrent assertions. The structure seems to be broken here. CHANGE; The section title is changed to "Concurrent assertions overview" Section 17.5 Sequences, first paragraph (end of pg 164) - second sentence: 'those specific points in time' are the corresponding clock ticks, aren't they? If we go through the whole subsection 17.4, why is this then not used here ??? - third sentence: 'one unit', again I think what is meant is one clock tick ?? CHANGE: Sentence changed to "These boolean expressions must be true at those specific clock ticks for the sequence to be true over time" and unit changed to one clock cycle Section 17.5 Sequences, second paragraph (start of page 165) - second sentence 'The concatenation specifies a delay between the two boolean expressions' sounds interesting. A delay between expressions? Consider rephrasing to 'The concatenation specifies a delay of one clock tick between the evaluation of the two boolean expressions' CHANGE: setence rephrased as "The concatenation specifies a delay, using ##, between the occurence two boolean expressions." - agree to Editor's note about 'compile-time constant expression'. Suggest to rephrase to 'a constant expression, where the actual value can be calculated {before simulation|during elaboration|during compilation|whatsoever}' CANGE: Sentence rephrased as "constant_expression is computed at compile time and must result in an integer value" Section 17.5 Sequences, first paragraph after bullet list following Syntax 17-3 (second third of page 165) - "is checked at the first occurence of the clock ...". Why do we define clock ticks when we don't use it here? CHANGE: "clock" changed to "clock tick" - "or after the element" _element_ is not defined within the BNF (only sequence_element), what is meant here ? When this is a recursive definition that this should be stated with a reference to the later definition of element ... CHANGE: element changed to expression Section 17.5 Sequences, second paragraph after bullet list following Syntax 17-3 (end of page 165) - ## is followed by a cycle delay range, but just using range sounds weird when there is a single expression; why don't state this is a cycle delay or a range (like the BNF suggests ...)? CHANGE: Changed "range" to "number or range". - Looking at the _new_ BNF from Stephen I think cycle_delay_range is over-specified: const_range_expression also includes the singular constant_expression (Is this BNF LALR(1)???) - example below this paragraph: the second bracket within the ##[0:3] a example uses 1 instead of 'true. Is this intentional? RESPONSE: This has been fixed. 1 changed to true - Last example before Figure 17-2 says #22, but the text says _second_ subsequent sample. Suggest to remove on of the two '2' and change 'subsequence' to 'subsequent' RESPONSE: This has been fixed. Section 17.5 Sequences, middle of page 166, after Figure 17-2 - second example: this example doesn't tell at all how the relationship between the first two lines and seq1,seq2 are being built. Is there something missing??? RESPONSE: First two lines indicate in comments that that they specify seq1 and seq2. - third example: what is the difference between using '&&' and ##0. None? Isn't '&&' also an operator? Then I could interpret c&&d as a single _expression_ which is clearly different from what is told here ... RESPONSE: ##0 fuses the end point and start points of the two sequences. When fused, the last expression of the first sequence and the first expression of the second sequence must occur at the same time. && is the boolean operator to indicate that the two expressions must be true. - last example on this page: "The time window can _be_extended_" Section 17.6 Declaring Sequences, start of page 168 - first bullet list, say 'an expression' and 'an event control expression' - before the bullet list, you say parameter (where Stu indicated that parameter has some meaning in Verilog) after the bullet list 'formal arguments' is used. Suggest to stay consistent. - third declaration of a sequence on this page: 'nededge' should use 'negedge' RESPONSE: These errors have been fixed. Section 17.6 Declaring Sequences, middle of page 168 - A sequence can be referenced in a property, an assert statement or a cover statement. a) assert is a keyword as well and should be marked like cover b) cover is not defined yet ... c) what is a property (same as assertion, see 17.1), this is also not defined yet hmmm. there is something broken here ??? RESPONSE: It is the style of Verilog manual, where not everything is defined before mentioned. Here is is only important to mention where a sequence can be used. CHANGE: bold used for property and cover. Section 17.6 Declaring Sequences, lower half of page 168 - possible problem??? Assume there is a name in a sub-sequence that is a formal argument of the enclosing sequence. According to the rule at the top this name is not provided by the enclosing sequence, but by the scope in which the sequence is instantiated. I assume this is intentional, but should be clearly spelled out. RESPONSE: This has been changed to " in which the sequence is declared" - The last paragraph of this page is broken. Section 17.6 last example before 17.7 - Why do we use a system task not yet defined ($rose()) for this example. Any other statement would have done it as well. RESPONSE; Apparently, the example is no longer there in the current version Section 17.7, page 170 - clearly state that example 1 and 2 are equivalent - consider moving the third example to be the first one. Don't bring a more complicated one before the most simple one. - the last example on this page implies that a[* 0] -- besides that the star is _before_ the square brackets in this example -- is equivalent to a non-existing sequence element. This is nowwhere spelled out ... Section 17.7, page 171 - Why do we specify several examples before defining the rules? We could define the rules and use the examples to illustrate them. This would be much clearer IMHO - again the rules imply that [*0] implies an empty sequence (repeat count) without saying this RESPONSE The following three bullets provide teh meaning of *0 - The sequence as a whole cannot be empty - If n is 0, then there must be either a prefix, or a post fix concatenation term to the repeated sequence - The match should not be empty CHANGE: A sentence added "Using 0 as the repetition number, an empty sequence results, as: a [*0]" Section 17.7, page 171 - I am sorry, but I am unable to grasp the difference between [*N:M] and [*->N:M]; especially the comment after the corresponding example is confusing. - The naming of the operator *-> is rather hidden (non-consecutive exact repetition) - Similar applies to *= - Q: Would it not be possible to describe the exact behavior of these operators? It takes some time to fully understand the syntax... RESPONSE: The tranformation to consecutive is provided, which describes the exact behavior. The names have been changed to align with PSL - General comment to the BNF inserts: Syntax 17-1, ... , Syntax 17-11, ... I would consider to name those inserts in a consistent manner; example for the current inconsistencies: . Syntax 17-10 first_match operator syntax . Syntax 17-11 throughout construct syntax (is this no operator ?) . Syntax 17-12 Sequence within another sequence syntax (isn't this the 'within operator') CHANGE: These have been corrected Section 17.7.2 page 172 - all subsections within 17.7 'hang' somewhat in the air, it is not easy to find out what is the relationship between all these elements. Why is this not being described somewhere in an introduction to 17.7??? RESPONSE: Section 17.7 describes the sequence expression operators. What relationship is missing? - all these definitions are missing some statement like "since the previous clock tick", which is an essential part of the definition RESPONSE: It is not clear what is the suggestion. - What about changes from Z to 1 or Z to 0, not to mention X to 1 .... According to the definitions all these are false. Is this intentional? RESPONSE: The sematics are similar to posedge and negedge, except that the values are between two successive clock ticks. - $stable seems to be related to the full breath of bits in the expression, no longer only the LSB. Assume this is also intentional? RESPONSE: If there is any change in any of the bits, then $stable returns false. - last paragraph before 17.7.3. Mentioning a clock different from the simulation ticks without saying what this clock is is confusing. Why are we not just refering to the assertion clock ticks here? At least we should say what _is_ the clock used; not only that it is different from something else. CHANGE: The text rephrased as "The clock ticks used for sampling the variables are derived from the clock for the property, which is different from the simulation ticks. Assume, for now, that this clock is defined elsewhere." Figure 17-4 - the expression te3 ##2 te4 ##2 te5 strikes twice (also at clock tick 6). The figure does not reflect this. - as a result the corresponding statements below this figure might be a little bit misleading/wrong () or I don't understand them ... Even when the text states that the evaluation attempt at clock tick 8 is shown, we should correctly show _all_ events. - Figure 17-5 suffers from the same problem. It should show the expression te3 ##2 te4 ##2 te5 to also strike at clock tick 6. - Figure 17-8 suffers from the same problem. It should show the expression te3 ##2 te4 ##2 te5 to also strike at clock tick 6 and also strike at clock tick 13. Also the OR of this expression will also strike at clock tick 6 and 13. - Figure 17-9 suffers from a similar problem. It should show the expression te3 ##2 te4 ##2 te5 to also strike at clock tick 6. Also the OR of this expression will also strike at clock tick 6. RESPONSE: This was done to avoid cluttering of the figure. 17.7.4 Intersection - I am sorry for my ignorance, but what is the length of a sequence ??? I would have expected that this is defined, when it is an essential requirement. RESPONSe: Th elength of a sequence is the duration of time for the sequence in terms of clock ticks. - Also, but this is more from a language design viewpoint: we do have an intersect, but no union ? why ? RESPONSE: We are or "or" is more appropriate than union for sequence operation Text at the end of page 174. - Figure 17-6 shows that the expression matches at clock tick 1,3, 8, and 14 (the last one misses in the text) RESPONSE: This is fixed Text below figure 17-7 - I have no idea why it is needed to compute the union of the two groups to calculate the result of an OR expression. I also don't understand why this is of interest for a user. What is the intention of this paragraph. RESPONSe: A sequence expression, in general, can result in more than one sequence. "or" calculates union of the sequences resulting from both branches. All sequences must be considered, since some of them may drop out due to other sequence operations on the result. Text at the end of page 178 - Please consider to more strongly link the note with the following example (continued at next page). Without this example it is impossible to understand it. CHANGE: The note is deleted. Example before 17.7.7 - I have no idea why it is important that two matches are ending at the same time when discussing the first_match operator ??? - So what is the conclusion of this statement. Is there something missing. Or why is this important (besides the fact that these are folded together as described earlier?) RESPONSE: The point is that first_match can result in more than one sequence. This happens when there are simultaneous matches at the earliest match point. 17.7.7 Conditions over sequences, end of page 179 - what is "a property stated over this composite sequence" ??? How to do this ? CHANGE: The sentence rephrased as "If either the ssequence_expr does not match or the expression becomes false while the sequence_expr is being evaluated, the sequence does not match." Text at the beginning of page 180 - This is very like caused by my limited understanding of the 'intersect' operator ... OR that I still don't understand what is the _length_ of a sequence ... - BUT: when this statement (throughout is an abbreviation for ...) is true, then a) either (boolean_expr) [*0:$] defines a sequence of _any_ possible length OR b) sequence_expr must have the same length as the sequence '(boolean_expr) [*0:$]' which I would consider as impossible for any sequence_expr Where am I wrong here? RESPONSE: Expression (boolean_expr) [*0:$] creates sequences of all lenghts (durations). Out of these dequences, only those will succeed that have the same length as sequences created by sequence_expr. Figure 17-10, 17-11 and 17-12 - The signal (trdy==0) and (irdy==0) should very likely be named (trdy==0) && (irdy==0) in Figure 17-10 (&& instead of and) RESPONSE: This has been fixed. - Why is (trdy==0) and (irdy==0) true in clock tick 11 in Figure 17-11, but not true in Figure 17-12 RSPONSE: This has been fixed 17.7.8 Sequence occurrence within another sequence - An example would be extremely useful here - the abbreviation statement kills me: how is it possible that a sequence contained within another sequence has the same length as the enclosing sequence ? (what the hell is the length of a sequence???) RESPONSE: Containment of a sequence is stated as : - The sequence sequence_expr1 must occur at least once entirely within the sequence sequence_expr2. That is, sequence_expr1 must satisfy the following: - The start point of sequence_expr1 must be between the start point and the end point (start and end point being inclusive) of sequence_expr2. - The end point of sequence_expr1 must be between the start point and the end point (start and end point being inclusive) of sequence_expr2. 17.7.9 Detecting and using endpoint of a sequence - is the .ended method true for only the clock tick when the sequence ended or also for any clock tick _after_ this clock tick RESPONSE: It is true only at the clock tick when it ended - what about sequences having multiple attempts? Is it true whenever an attempt ended ? Please clarify RESPONSE: Yes. - page 182 top of page: the two sentences starting with "If the method ended wasn't there, " could be more clearly worded and do not add much (usage of sub-sequences has already been described) CHANGE: The sentence rephrased as: "If the method ended is replaced with sequence e1, e1 must start one clock tick after inst" 17.7.10 Implication - where is 'antecedent sequence_expr' and 'consequent sequence_expr' being defined, Annex A doesn't describe it and the text either. I also don't understand why this is in italics? I have further talked to some of my native english speaking peers, most of them understand antecedent and consequent from the context, but would not use it without further explanation what it is within an implication definition. CHANGE: A sentence added: " The left hand side operand sequence_expr is called antecedent, while the right hand side operand sequence_expr is called consequent." - is not a separate operator like and,or or is it a part of the implication operator and only permitted here (I assume so). If yes then this is interesting syntax ... - I doubt that without knowledge about temporal logic it is possible to understand the newly inserted points noted for the implication - the text uses sequence_expr while Annex A uses sequence_spec? RESPONSE: This has been fixed Property below figure 17-12 - defines data_end, but uses data_end1 - given the possibility to define a sequence for data_end I would consider usage of 'define as being ancient, why is this not also defined itself as sequence ? RESPONSE: This has been fixed. The reason to use macro is that the expression is just a boolean, and not a sequence. Although, you could define it as a sequence. Figure 17-14 is confusing. I would be better to just show every value of data_end_rule2. What should that boxes and arrows tell me ??? RESONSE: The arrows show success/failure, while the dotted box shows time window. Page 185: - Does the last example now introduce a property block (unfortunately the BNF is not yet updated). - would it not be better to move this example to 17.11 ? RESPONSE: It just shows a more complicated implication in a property definition. Section 17.8 - From now on there is a lot of property blocks used without declaring it. This is done in 17.11. - Iff it would be possible to use sequence here as well as property then we should do it. It is very hard to understand the local variable descriptions due to missing information or special names, notations; examples: - accumulation of values: it would be good to state what is the result (guess: sum of the last four 'data' values before ##1 b ##1 c ...) RESPONSE: The assignment gets repeated. If the variable is used in lhs for assignemnt, then the value gets carried over from one iteration to another, and possible accumulated. - special considerations 1): 1) what constitutes a parallel branch RESPONSE: or, and and intersect have two operand expressions that get evaluated simultaneously. This is referred to as parallel branches. 2) what is the difference to a parallel thread RESPONSE: Difference in the variables assigned. 3) how do I as a dumb user identify a sibling thread (just playing devil's advocate) RESPONSE: sibling threads are the parallel threads. 4) I assume the usage of || is illegal; it should be or ??? RESPONSE: I resume you mean or. The use is not illegal, but there are rules of what is visble after the or operation. - special considerations 2): what would be the value of x in the comparison, if x got different assignments in both threads? I assume this is permitted, it is at least not forbidden ;-) - special considerations 3): I assume it is meant to say "In the case of and and intersect, ..." RESPONSE: There is some complicated description in this section. Given enough time, it can be presented better. Section 17.10 - Is the replacement of the formal arguments for a property statement done like it is for sequences (syntactical replacement)? RESPONSE: YES. - Do the same rules apply for arguments not defined as formal arguments - When do I use sequence, and when do I use property; it looks like property is just a shorthand for first_match(sequence) ??? RESPONSE: Also, you can have implication, resets and negation. Sequences are used to build a property. Property is what gets asserted(checked). Section 17.11 - last paragraph on page 191, 'desalination', what's this? Especially what salt is removed by e1 ;-) ??? RESPONSE: type fixed; destination - similar to ended, .matched is only true when a) the corresponding sequence is .ended at exactly(?) the arrival of the first destination clock tick after the source clock tick b) what is the value, if there is one or more source clock ticks before the arrival of the destination clock tick RESPONSE: It stays true until the arrival of destination clock. Section 17.12 top of page 192, - second paragraph: what is the severity when I overrride the default $error _without_ having another system function defining such a severity RESPONSE: No severity. If else action is specified, then it is up to the user. - there is a dangling or at the end of the second cover property statement description (middle of page 192) - shouldn't the syntax definitions described end up in the BNF ? This is not the case for the ones in the middle of page 192 - end of page 192: What is the _result_ of a coverage statement (is this a class, a specific data type or what). If this is the data to be made available by a cover statement, then this sentence needs to be rephrased to state this. The data is described is for reporting. Tools may decide how to present the data. Using VPI, one can get this data. - what is the meaning of '(limited)' after 'because of vacuity' ? The word limited is deleted. - vacuity is used before, but not really well defined ??? Is the "definition" of non-vacuously on top of page 193 an attempt to solve this ? I am unsure why it is needed to use this term RESPONSE: The following sentence describes it: "A property succeeds non-vacuously only if the consequent of the implication contributes to the success." -- the name 'property coverage' is confusing, since property statements are used also for sequence coverage. So there is the property construct used for defining property coverage and sequence coverage. Uggh RESPONSE: Yes. Section 17.12.1/2 - Sorry, but I missed the point when to use always ??? - Is there now a difference when I use always instead of omitting it ? - Is always needed to denote a concurrent assertion statement ? - If I specify an assertion statement within a module/interface when is it evaluated (always is not the right answer here ...) a) when the module code is executed b) anytime else if I put now always in front of the assertion does this change something ??? - also overriding inferred clocks seems to be not very intuitive Significantly confused, sorry RESPONSE: There are two modes in which a concurrent assertion is evaluated: 1) initial - evaluated only once on the first clock tick 2) always - evaluated at every clock tick If the assertions appears in an always block, it is 2). If it appears in initial, then it is 1). If the assertion appears outside of procedual blocks, then it is 2)