Section 17.3: As with the if statement, if the expression evaluates to X, Z or 0, then the assertion fails. Q: Are only 1 bit expressions allowed in the assertion clause? If any width is allowed, this paragraph should just say these act like any other conditional context. CHANGE: The sentence has been changed as below "The statement associated with the success of the assert statement is called the pass statement, and is executed if the expression evaluates to true. The evaluation of the expression follows the same semantics as that of the conditional context of the if statement. As with the if statement, if the conditional expression evaluates to X, Z or 0, then the assertion fails." $fatal is a run-time fatal, which terminates the simulation with an error code. The first argument passed to $fatal shall be consistent with the argument to $finish. Q: Why is the first argument "n" only for $fatal? Why isn't it used for $error, $warning and $info? At least the values of 0 and 1 are meaningful for them. RESPONSE: $fatal terminates the simulation, while others are just run-time errors. NO Change Q: Which kind of expression can you have in a immediate assertion? Does it have to be a boolean expression? Can you have a sequence? RESPONSE: "expression" production is defined in System verilog and is non-temporal. CHANGE: The sentence has been modified as "The expression is non-temporal and treated as a condition as in an if statement." Section 17.4: Q: there is no bnf for concurrent assertions, are they the same as the immediate assertions but are concurrent? RESPONSE: SEction 17.12 describes the BNF for concurrent assertions. CHANGE: The title of 17.4 has been changes to Concurrent assertions overview, an example of concurrent assertions has been added, and the reference to section 17.12 is provided for full BNF discussion. Section 17.5 I think the bnf is incorrect. sequence_expr ::= [ cycle_delay_range ] sequence_expr { cycle_delay_range sequence_expression } I think that the last item on the derivation rule should be sequence_expr. CHANGE: sequence_expression has been changed to sequence_expr Section 17.5 page 165: A range of 0 specifies that the next element should occur in parallel with the current cycle. I would prefer to read "within the current cycle". RESPONSE: Within the cycle would be ok only if the next element is a boolean and does not have any range. In parallel, means that the next element starts at the current cycle. No Change. Q: Why requiring to specify 0? why not allowing " a b" instead of a ##0 b? RESPONSE: To have a different syntax would disallow parameterization of delays. For example, one couldn't write a ##n b, where n is a parameter. No Change "The following are examples of unary delay expressions. true is used to indicate that the expression is true." Q: Why qualifiying the delay expressions of unary? They are just delayed expressions. ## t is used in SystemVerilog and it is refered to as a delay expression RESPONSE: Semantics of delay when used in a unary context were not clear to many, so the word unary has been used. No Change. I found the equivalency defined between ##x and 'true complicated to read and understand. I understand perfectly ##2 a as meaning 2 cycles later "a" should be true. The equivalent transformation to sequences of 'true is more complex to understand. I would suggest removing this equivalence description. RESPONSE: The description was reviewed in the committee and agreed to keep it as it clarified different scenarios of delay operations. No Change Page 166: example does not match explanation. This specifies that req will be true on the current sample, and gnt will be true on the second subsequence sample, as shown in Figure 17-2. req ##22 gnt CHANGE: 22 changed to 2 Q: Why is a sequence_expr called a concatenation; this is very unlike verilog normal concatenations. I would prefer to not reuse the word concatenation to specify a sequence to expressions. It is very confusing. RESPONSE: The word concatenation is well understood operation on sequences that extend the length of sequences, that is one after the other. Similar meaning is used in Verilog on bit-vectors to extend the length. Though, overlapped concatenation is pecular only to sequences, due to timing aspect. No Change. Page 166, just below the figure: To specify a concatenation of overlapped sequences, where the end point of one sequence coincides with the start of the next sequence, a value of 0 is used, as shown below. a ##1 b ##1 c // first sequence seq1 d ##1 e ##1 f // second sequence seq2 seq1 ##0 seq2 // overlapped concatenation This is not the general meaning of overlap, it only overlaps for 1 tick. Overlap means that there is an intersection between the times where the sequence 1 would start and the sequence 2 would start. I would rather qualify this of sequential sequences, where seq2 starts exactly when seq1 ends. RESPONSE:The following setence already clarifies your point: "To specify a concatenation of overlapped sequences, where the end point of one sequence coincides with the start of the next sequence, a value of 0 is used, as shown below." When concatenated with 0 sampling, c and d must occur at the same time, resulting in the concatenated sequence being is equivalent to: a ##1 b ##1 c&&d ##1 e ##1 f CHANGE: Following sentence has been added to further clarify: "It should be noted that no other form of overlapping between the sequences can be expressed using the concatenation operation." I am also assuming that we are declaring seq1 to be a ##1 b ##1 c. This is not shown in the example. RESPONSE: This is mentioned in the example comments a ##1 b ##1 c // first sequence seq1 d ##1 e ##1 f // second sequence seq2 No Change Q: Isn't the above also equivalent to: a ##1 b ##1 c ##0 d ##1 e ##1 f RESPONSE: Yes. No Change Page 167 (just above section 17.6) A sequence can be unconditionally extended by using true. a ##1 b ##1 c ##3 true After signal c, the signal length is extended by 3 sample events. Such adjustments in the length of sequences are required when complex sequences constructed by combining simpler sequences. The signal length is not extended. The signal c does not need to remain high for 3 events later. what does ## 3 means is that there are 3 clock ticks happening after c becomes high. I really don't see why this is necessary, since you can accomplish the same by using ## 3 between seq1 and seq2. If seq1 is a ##1 b ##1 c and seq2 is d. I can write seq1 ## 3 seq2 and have the exact same behaviour as with seq1 is a ##1 b ##1 c ##3 true seq 3 is d seq1 ##0 seq3 RESPONSE: Yes, in your case it is ok since you know the following sequence seq3. But, when the sequence is written independently, the total length is part of the sequence itself. The sequence may or may not be used in concatenation. CHANGE: Typo "signal length" is changed to "sequence length". Section 17.6 page 168: a name that is not a definition name Q: What is a definition name? CHANGE: The sentence is changed to "identifier" Section 17.7.1 repetition sequences "Following is the syntax for sequence concatenation (sequence_phrase from concatenation has been extended with repetition clauses)." I don't understand why we have a title "repetition sequences "and the first sentence refers to sequence concatenation. I like better repetition sequence because concatenation is used in a completely different way in Verilog. Q: What is sequence_phase? why is it in italic? CHANGE: The sentence is changed to: "Following is the syntax for sequence repetition." "The repetition counts are specified with range and must be literals or constant expressions." I would rewrite this as: The repetition counts are specified as a range and the range min and max expressions must be literals or constant expressions. CHANGE: The sentence has been changed to: "The repetition counts are specified as a range and the minimum and maximum range expressions must be literals or constant expressions" page 170: typo: which which means CHANGE: Removed "which" page 170: If n is 0, then there must be either a prefix, or a post fix concatenation term Q: Why do we need a post fix? We need to define what is the prefix and post fix concatenation item. I am guessing that the post fix is the sequence expression after the repetition count. What is the prefix and post fix of this sequence. a ##1 b [*2] ##1 c RESPONSE: Here, the prefix is "a ##1 true" , and the postfix is "#1 c". CHANGE: The sentence changed to: "If n is 0, then there must be either a prefix, or a post fix concatenation term to the repeated sequence" Page 171: This is equivalent to: a ##1 ((!b [*0:$] ##1 b)) [*min:max]) ##[0:$] !b ##1 c It would be useful to provide a sequence of a, b, c which is true for the above sequence expression. ex: a c c c c b c c b c b d d d c this is a sequence which will pass the above sequence expression, assuming 3 is contained within the range min: max. CHANGE: Following example added "The above expression would pass the following sequence, assuming that 3 is within the min:max range. a c c c c b c c b c b d d d c" Section 17.7.2: $rose, $fell, $stable Q: why are these past tense rather than $rise, $fall? RESPONSE: These words were reviewd by SV-AC and the ASWG committees and voted. No Change Section 17.7.3: I have the same remark as the editor. Why not using &? RESONSE: This issue of using && for "and". || for "or" and ! for "not" was discussed at length, and ASWG voted to keep these words. The reasoning was that the sequence operations are different than boolean operations, and disambiguating them syntactically was inportant. No Change Page 174: An example is illustrated in Figure 17-6 to which shows the results for attempt at every clock tick. The expression matches at clock tick 1, 3 and 8, because both te1 and te2 are simultaneously true. At all other clock ticks, the and operation fails because either te1 or te2 is false. I think te1 and te2 succeeds also at clock tick 14. CHANGE: The sentence is changed to "matches at clock tick 1, 3, 8, and 14....." Section 17.7.4: An example would be welcome. Section 17.7.6: For a given evaluation attempt, the composite expression matches if sequence_phrase results in at least one match of a sequence, and fails to match if none of the sequences from the expression result in a match. Q: What is sequence phrase?, What is the composite expression? I cannot correlate the bnf specified as first_match(sequence_expr) with the above description. CHANGE: The word "sequence_phrase" changed to "sequence_expr" I don't understand what the note means: Note that first_match applies to each attempt for the sequence individually. CHANGE: The note is removed. Page 179 (last example): As another example: sequence t2; (a ##[2:3] b) or (c ##[1:2] d); endsequence sequence ts2; first_match(ts2); endsequence Each attempt of sequence t2 can result in matches for up to four following sequences: a ##2 b a ##3 b c ##1 d c ##2 d Sequence ts2 results in the earliest match. In this case, it is possible to have two matches ending at the same time. a ##2 b c ##2 d I think the last comment is very confusing. We should rewrite it and say that it is possible to have 2 first match a ##2 b , c ##2 d IFF a and c are true at the same clock tick and these sequences are the earliest match sequences. (it is not possible to choose between them because they are first match). CHANGE: A sentence added. "In this case, first_match results in two sequences" Section 17.7.7 Page 180 figure 17.10 The figure says trdy = 0 and irdy = 0 but the sequence expression is trdy= 0 & irdy = 0 Both should use the same, whichever is correct. CHANGE: Figure is corrected. It should be "trdy && irdy" Section 17.7.8 syntax table 17.12 I think that the syntax should instead be sequence_expr ::= sequence_expr1 within sequence_expr2 which uses 2 different identifiers for the sequence_expr. RESPONSE: In the BNF, it is sufficient to say sequence_expr. But for discussion it is needed to use the two identifiers. No Change. Section 17.7.10: Q: why using a method rather than a system task $end? RESPONSE: We did have this option. But ASWG had the preference of defining it as a method. Also, a system function can be redefined using a PLI call with the same name. A system method is pre-defined and cannot be changed. Section 17.7.10: I am assuming that the final bnf uses antecedent_sequence_expr and consequent_sequence_expr. Page 183: boolean_expr |=> [not] sequence_spec is equivalent to: boolean_expr ##1 true |-> [not] sequence_spec Sequence_spec should instead be sequence_expr The not operator should be described before the implication section. It is not described at all. CHANGE: The description changed to "sequence_expr |=> [not] sequence_expr is equivalent to: sequence_expr ##1 ‘true |-> [not] sequence_expr If not is used on the consequent, the result of consequent sequence_expr is reversed" Page 183: typo Each time a data phase completes, a match for data_end is recognized. The Should be data_phase. CHANGE Stntence changed to "Each time a data phase is true, a match for data_phase is recognized." page 183: example A property is written to express this condition as shown below. define data_end (data_phase &&((irdy==0)&&($fell(trdy)||$fell(stop)))) property data_end_rule1; @(posedge mclk) data_end1 |-> ##[1:2] $rose(frame) ##1 $rose(irdy); endproperty Q: Why is the example using data_end1 instead of data_end? RESPONSE: data_end is a property, so it cannot be used in another property. CHANGE data_end macro name changed to data_end_exp Q: Why are we using a macro instead of a sequence declaration? RESPONSE: We could write it as a sequence. This is a short cut, since th eexpression is basically a boolean expression. No Change Q: What is the meaning of de-asserted in the following sentence, this is the first time this verb is used? data_end can be used to ensure that frame is de-asserted within 2 clock ticks after data_end occurs. Further, it is also required that irdy gets de-asserted one clock tick after frame gets de-asserted. CHANGE; This has been removed. page 185: An example of sequential implication is: (a ##1 b ##1 c) |-> (d ##1 e) Q: Why are we using the term of sequential implication? It is the first time introduced. It should be called non overlap implication instead. CHANGE: The sentence changed to "An example of implication where the antecedent is a sequence expression is" Page 185 Last example property p16; (write_en & data_valid) ##0 (write_en && (retire_address[0:4]==addr)) [*1] |-> ##[3:8] write_en && !data_valid &&(write_address[0:4]==addr); endproperty Q: Is the first line of the property write_en & data_valid or should it be an &&. RESPONSE: Although the example does not declare signal, presumably, it is a multi-bit expression. No Change Section 17.8 page 186 property e; int x; (valid_in,(x = pipe_in)) |-> ##5 (pipe_out1 == (x+1)); endproperty A formal description of the behaviour of the above property would help understand: The property evaluates to TRUE if : if (valid_in) x = pipe_in and 5 clock ticks later, pipe_out1 should be equal to x+1. or !valid_in (valid_in is FALSE) The property evaluates to FALSE if valid_in is TRUE, x = pipe_in and 5 clock ticks later, pipe_out1 is not equal to x+1. CHANGE: Following is added "Property e is evaluated as : When valid_in is true, x is assigned to pipe_in. Property e is true if five cycles later, pipe_out1 is equal to (x+1). Proeprty e is false if pipe_out1 is not equal to (x+1). When valid_in is false, proeprty e evaluates to true." I think the following needs to be reworded: 1) Variables assigned on parallel threads cannot be accessed in sibling threads. For example: sequence s4; int x; (a ##1 b, (x = data) ##1 c) || (d ##1 (e==x)); // illegal endsequence The issue is that if you assign a variable in one sequence, you cannot read it in another parallel sequence. Note that you could assign x in both sequence and we would have 2 instantiations of c. RESPONSE: No suggestion. No Change Page 186: in bullet 2) Wording is terribly confusing: Intersection was defined before as an operator on sequences. we should not use this term for describing this. 2) In the case of or, it is the intersection of the variables (names) that passes on past or. More precisely, a local variable passes on past the or if and only if, either a) The local variable exists at the start of or, or =====> this is not great. RESOLUTION: Explicit meaning is provided in a) and b). No suggestion. No Change Page 186 in Bullet 3, there is a mistmatch use of "&&" and "and" Q: Which one is correct? CHANGE: && corrected to "and" The description is quite confusing. There is no definition of what is the symmetry difference. RESOLUTION: Explicit meaning is provided in a) and b). No suggestion. No Change Q: What is the effect of assigning a value of data to x and reading x in another sequence? RESPONSE: If the data passes according to the rules described, then x will have the values assigned in the previous sequence. Q: Which value would I get for x? RESPONSE: It's hard to say in general. Using th e rules described, One can figure out. Example: sequence s8; int x,y; (a ##1 b, x = data, y = data1 ##1 c) and (d ##1 true, x = data ##0 (e==x))) ##1 (y==data2); // legal since y is in the difference endsequence In the above sequence, is it expected that e is equal to data 2 ticks after d is true? RESPONSE: data is assigned to x first, and compared in the same tick (##0) to e. The computation of intersection and difference of set of names should be demonstrated in that section. It is not clear what this means at all. RESPONSE: Perhaps, an example is needed. No Change Section 17.8 typo: The variable may be assigned any where in the sequence, any where is one word. CHANGE: Changed to anywhere Q: Are the local variables sampled on a clock domain? If yes, why are the names not relative to the clock domain. That will make it more easy to understand which local variable value is used. Please describe what is the intersection of variable names and the symmetric difference and how these are computed. Sentences such as : "In the case of or, it is the intersection of the variables (names) that passes on past or." or "the symmetric difference of the local variables that are sampled in the two joining threads passes on past the join." are not clear at all. RESPONSE: It is the intersection of sets of names from the two branches. Names refer to the local variables that are assigned.Symmetric difference is the difference of the two sets of names. What is the join? This is the first time it is mentioned in bullet 3: The value passed on is the latest sampled value. The two joining threads are merged into one thread at the join. RESPONSE: join refers to the joining of the two threads, such as ((a ##1 b) and (c ##3 d)) ##4 d. Two threads are (a ##1 b) and (c ##3 d), and they join when the expression ((a ##1 b) and (c ##3 d)) completes. sequence s8; int x,y; (a ##1 b, x = data, y = data1 ##1 c) and (d ##1 ‘true, x = data ##0 (e==x))) ##1 (y==data2); // legal since y is in the difference endsequence Assuming data is sampled to be 0, in the left sequence expression of the "and" , x will be set to 0. Then at the next clock tick, data changes to 1, does this changes the value of x in the left sequence? RESPONSE: No. The x remains unchanged until reassigned in the same branch. What about the value of x in the right sequence expression? is it also 0? RESPONSE: x on the right side is a different instance of x. It is assigned to data, and that is the value. What about if the right sequence assigns data to x a clock tick later when data is equal to 1: RESPONSE: Since the x on right sequence is a different instance of x, its value is determined according to the assignmnet on the right sequence. (d ##1 ‘true ##1 x = data ##0 (e==x))) ##1 (y==data2); Do we have 2 instances of x, one for the left sequence and one for the right sequence, the left and right x have 2 different values? or is there only one instance of local variable x and the value of x is the last assigned value (1 in this exmaple). RESPONSE: Yes, as explained above. This section needs lot of formal clarifications and needs to be complemented with examples. RESPONSE: Agreed. No Change at the moment. Section 17.9 System Functions I noticed here again the use of a $task. It seems that there is a mix of use of systemfunctions and method in the assertion syntax (.ended). What is the reason for choosing one or another? Can we be consistent? ReSPONSE: These functions operate on an expression, while ended operates on a sequence. There is no syntax for a method on an expression. No Change $countones seems like a general purpose system function which should not be in the assertion chapter but in section 22. RESPONSE: That is right. These functions will be accepted in any expression. No Change Section 17.10 Properties A lot of clarifications on the terms used need to added to this section. "A property declaration is parameterized, like a sequence declaration. When a property is instantiated, actual arguments can be passed to the property. The property gets expanded with the actual arguments by replacing the formal arguments with the actual arguments. The semantic checks are performed to ensure that the expanded property with the actual arguments is legal." Q: which semantics checks are performed? RESPONSE: There are numerous checks, such as variable compatibility, clocking, sequence operations, etc. The checks would depend on the property/sequence expresssion. Note that the data types of formal arguments are not known until expanded. No Change Q: can you pass actual arguments of different type than the formals? RESPONSE: No data types are declared. The requirement is that they must conform to event expression (identifier, expression and edge expressions) No Change Q: can you pass local variables as actual arguments? If yes, how do you specify the type of the local variable? RESPONSE: You declare the local variable in the property/sequence from where it is passed down to. No Change Q: how do you instantiate the property? Is the property declaration an instantiation? RESPONSE: A property is instantiated in an assert or cover statement by invoking with real arguments, such as assert property (p2(a,b,c)); // p2 is a property that takes three formal argument Section 17.10 page 198: The result of property evaluation is either true or false. If the property is just a sequence, the result of a sequence for every evaluation attempt is true or false. If the property is just a sequence, the result of a sequence for every evaluation attempt is true or false. This is accomplished by implicitly transforming sequence_expr to first_match(sequence_expr). That is, as soon as a match of sequence_expr is determined, the result is considered to be true, and no other matches are required for that evaluation attempt. Q: when is a property evaluated? Nothing is said about this. A property declaration does not evaluate the property. RESPONSE: Property is evaluated based on the assert statement usage. There are two cases: always, where it is evaluated on every clock tick, and initial, where it is evaluated only on the first clock tick. No Change Q: The text "If the property is just a sequence, the result of a sequence for every evaluation attempt is true or false. This is accomplished by implicitly transforming sequence_expr to first_match(sequence_expr). " seems to indicate that the property is not evaluated any more after a match has been found. How do you create properties which state that the sequence must be true at ALL times? Personaly I don't like the implicit transformation. RESPONSE: As said before, property is evaluated always or once, based on the assert statement where it is instantiated. first_match on the sequence only specifies how a sequence is transformed to a property. There is a difference between saying a sequence has multiple possiblities of match(success) and a property being true at every clock tick. No Change The next sentence seems to say that there is a different behavior for the implication sequence: However, if the property is an implication, then the semantics of implication determine whether the property is true or false. Q: Is the first match implicit transformation done on the implication? Or a property with an implication sequence is evaluated on every sequence attempt? RESONSE: There are two kinds of property: one where it is just a sequence, second when it is an implication. These two cases are described. CHANGE: A sentence added: "There are two kinds of property: sequence, and implication." Disable iff (expr) This construct clearly needs a formal description of the logic behind it. Some kind of a truth table should be provided. RESPONSE: Formal semantics of properties and sequences are defined and available in a document. The formal semantics document will become an appendix in the final LRM. No Change Q: does the disable causes the property to not be evaluated any more if expr becomes true during the property evaluation? The text says that the property attempt succeeds but it does not say if it stops being further evaluated in other attempts. RESPONSE: Each attempt of property evaluation is considered separately. "disable iff" disables only the attempt when its expression is satisfied. CHANGE: A sentence added: "Other attempts are not affected by the evaluation of the expression for an attempt." The not clause states that the expression associated with the property must never evaluate to true. Effectively, it negates the property expression. For each attempt, clocked_sequence results in either true of false, based on whether there is a match for the sequence. The not clause reverses the result of clocked_sequence. It should be noted that there is no complementation or any form of negation for the sequence itself. The text should specify more precisely which expression is negated ( the one in the IFF or the property_expr following the NOT), especially because the property_expr appears in a syntax rule outside of the disable iff (expr) [not]. CHANGE: expression replaced with property_expr, which is a BNF production. Q: what is the meaning of "It should be noted that there is no complementation or any form of negation for the sequence itself." I would define the NOT as an operator on a sequence_expr. RESPONSE: Not on a sequence may imply that there is complementation on the sequence, which is different than just negating the result of a property. No Change I would add a description for the behavior of the example in this section: For the following example : property rule2; disable iff (foo) not @(clkev) a |-> b ##1 c ##1 d; endproperty the property evaluation for rule2 will succeed if the implication (@clkev...) is always FALSE or if foo is determined to be TRUE at a given clock tick during a sequence attempt. CHANGE: A sentence added: "Property rule2 negates the result of the implication (a |-> b ##1 c ##1 d) for every attempt." Q: What is the use of the example of property rule1? RESPONSE: Just an example of a property. No Change A property can optionally specify an event control for the clock. Q: Is there a relation between the event control for the clock and the clock ticks? Or is the event control adding an extra clock trigger for the start of the attempt, then every other match of the sequence expression is done on a regular clock tick? RESPONSE: There are many sources of a clock: such as when a property is declared in a clock domain, or instantiated in an assert within an always block, etc. When the property clock is not specified, other sources are examined to attach a clock. The clock resolution rules are described in a later section. CHANGE: A sentence added: "A property can optionally specify an event control for the clock.The clock derivation and resolution rules are described in Section 17.13." In the example for rule2, is each separate attempt of evaluation of the sequence @(clkec) a |-> b ##1 c ##1 d only started when clkev changes value? Are the values of a, b, c, d sampled on an external clock? By reading further on the clock resolution rules, I understand that clkec is the clock tick. A statement should be added to state it. CHANGE: A sentence added: "clkev specifies the clock for the property." Q: is this called a clocked sequence? if yes, then this notion of clocked sequence should be introduced here. or the sentence " A property can optionally specify an event control for the clock." should be moved to section 17.11 CHANGE: BNF has been changed, and text modified accordingly. Section 17.11: Multiple clock support Page 190: The multi-clock concatenation operator ## synchronizes between the two clocks. @(posedge clk) a ## @(posedge clk1) b The above is confusing, Verilog has 1 concatenation operator which is {}. We should not use the same term to designate 2 different things. RESPONSE: Concatenation of sequences has been explained and used throughout the chapter. Reader should be familiar by now. No Change. The 2 following examples are redundant. Only one is sufficient: When signal a matches at clock clk, ## moves the time to the nearest clock tick of clk1 after the match. At the first clock tick of clk1, it matches b. For two sequences, such as @(posedge clk) s ## @(posedge clk1) s1 For every match of s at clock clk, ## moves the time to the first clock tick of clk1. From that first tick of clk1, s1 is matched. RESPONSE: It is important to clarify that the multi-clock operation occurs for every match of teh lhs sequence. No Change Section 17.11.1: To detect the end point of a sequence when the clock of the source sequence is different than the desalination sequence, method matched on the source sequence is used. Q: please explain what is the desalination sequence. This is the first time the term is used. The above sentence does not flow very well (grammar). RESPONSE: a typo CHANGE: desalination changed to "destination" Q: I don't understand the reason for having a different method "matched" to be used to determine if a given sequence has reached the end point. It seems that Matched has to be used instead of ended only if the clocks in the 2 sequences are different. Why? RESPONSE: The semantics are different. The result of ended is applied in the expression on the same clock edge that it occurs. No synchronization is need. If the two clocks are identical, then there would be one clock tick difference between ended and matched. No Change Section 17.12 Concurrent assertions page 192: typo for a sequences. CHANGE: sequences changed to "sequence". incorrrect grammar: The assert and cover statements can be referenced by its optional name. CHANGE: its changed to "their" I think that semi-colons should be added at the end of each cover statement example: cover property ( [event_control] sequence_instance ) statement_or_null or cover property ( [event_control] sequence_expr ) statement_or_null, or RESPONSE: statement_or_null already has the semicolon. No Change The (limited) should instead be (limited to implications) and thus the sentence (Vacuity rules...) below can be eliminated. The results of coverage statement for a property shall contain: — Number of times attempted — Number of times succeeded — Number of times failed — Number of times succeeded because of vacuity (limited) — Each attempt with attemptID and time — Each success/failure with attemptID and time statement_or_null gets executed every time a property succeeds. Vacuity rules are applied only when implication operator is used. CHANGE: text "(limited)" deleted. Q: How and when are the results reported, accessed? RESPONSE: It is not defined. Tools may decide when to report. There is a mechanism to access the results using VPI. No Change Page 193: Change: A property succeeds non-vacuously only if the consequent of the implication contributes to the success. to: A property succeeds vacuously only if the antecedent of the implication is FALSE. (much simpler) RESPONSE: It is incorrect to say that a property will succeed, just because the antecedent succeeds.Generally, users are interested in knowing the non-vacuous successes. No Change Page 193: It is said that Results of coverage for a sequence shall include: — Number of times attempted — Number of times matched (each attempt can generate multiple matches) — statement_or_null gets executed for every match. If there are multiple matches at the same time, the statement gets executed multiple times, one for each match. Q: How can the result of coverage be the execution of the statement_or_null? (3rd ---) RESOLUTION: Action block is executed every time there the property is true. The results of coverage are reported regardless of the existence of the associated action block. CHANGE: The bullet separated out as a sentence. "In addition, statement_or_null gets executed for every match. If there are multiple matches at the same time, the statement gets executed multiple times, one for each match." Q: all these results seems to provide a lot of data. All of that data is mandatory according to the "shall" used in the sentence. Is it really mandatory, or should the verb "may" be used to provide more freedom to a tool. RESPONSE: The use of the word "may" makes the meaning of coverage optional. The tools always have means to deal with data accumulation and presentation. They may choose to present the data according to their own methods, and provide filtering. However, the semantics remain the same. No Change. Q: what is attemptID, what is clock step? is it an integer value? Needs to be precised. RESPONSe: Every attempt must have an identification, attemptID. Tools may choose any method to identify. clock step is the clock tick related to the occurence of the covered item. CHANGE:A sentence added: "attemptId is the identification of a particular attempt. Clock step is the clock tick of the occurrence of the match." Section 17.12.2 Page 194 I found this feature of having concurrent assertion hidden in procedural flow hard to conceptualize and to use: An assertion which is appearing in a procedural sequential flow in an always context is in fact a concurrent assertion. It is always checked, not just checked when the procedural flow encounters it. I think it is redundant with the other way of creating concurrent assertions. It does not add any capabilities, rather complicates the tool which have to implement these "false procedural assertions" because the tool has to calculate (infer) the conditions which trigger the assertion by computing the logic leading to the assertion stmt. I find it even more confusing when the inferred clock is overwritten by a clock specified in the property, then why putting that assert statement in an always block? RESPONSE: Embedding of assertions, and inferring has been discussed and voted in the SV-AC committee. CHANGE: The inferred clock is not overwritten by the explicit property clock. They both must be identical. The change has already been made. Page 195: In the example provided, the equivalent transformation of the procedural assertion into a concurrent assertion is very easy to understand however the inferred condition for the assertion can be very complicated to compute... Why are we allowing concurrent assertions in a sequential context? What does it solve that concurrent assertions with proper condition cannpot solve? RESPONSE: It saves from extracting conditions and putting them in properties, thereby, introducing unnecessary errors. Also, designers prefer to write assertions where the behavior occurs. It is expected that the notion of embedding concurrent assertions in procedural block will become intuitive, once users start writing assertions. No Change property r3; @(posedge sclk)(q != d); endproperty always @(posedge mclk) begin if (a) begin q <= d1; r3_p: assert r2; end end The above example is equivalent to: =====> Note that the code below has very clear behaviour while the code above is obscure to understand the condition for the assertion stmt. This is an argument against procedural assertions. property r3; @(posedge sclk)a |-> (q != d); endproperty r3_p: assert r3; always @(posedge mclk) begin if (a) begin q <= d1; end end Page 195: the further limitations on no timing control, no loop, no task call make me feel that this a very complex analysis of the Verilog code is required to determine the legality of procedural assertions. Was an implementation cost analysis versus usefulness conducted? RESPONSE: It is only compile time analysis, and simulators these days perform much more complicated analysis already. No Change Section 17.13: Clock resolution If clock domains are used, why not referring to the clocked domain sampled signals with a hierarchical name starting with the clock domain? Program blocks refer to them that way, why aren;t the assertions using the same? RESPONSE: When the property is declared within a clocking domain, there is no need to prefix it. Since properties are always clocked, it is much more convenient to specify clock once and use the ordinary names. No Change sequence s2; @(posedge clk) a ##2 b; endsequence property p2; not s2; assert p2; Q: in the above example, is the clock tick for the sequence "posedge clk"? I am guessing it it. May be this needs to be clarified in the clocked sequence section. RESPONSE: A clock tick refers to a single event, while posedge clk is the clock that generates clock ticks. The notion of a "clock" is already known to Verilog users, and it is not much different here in that regard. No Change Page 196: I don't see any difference in the way the clock is specified for the 3 following examples. For all 3, the clock is posedge clock and is specified for the sequence expression. After substitution of the sequence expression, the property clock tick is the posedge clock. — clocked_sequence, for example property p1; not @(posedge clk) a ##2 b; endproperty assert p1; — sequence_instance, for example RESPONSE: clocked_sequence production has been eliminated from the BNF. No Change — sequence s2; @(posedge clk) a ##2 b; endsequence property p2; not s2; assert p2; — property, for example property p3; @(posedge clk) not a ##2 b; endproperty assert p3; RESPONSE: In the above two, there are different usages of the clock specification. The rules are specified later. No Change Q: In the last example (property p3) , what is the meaning of not a ##2 b Is the not operator applying to a only or to the entire a ## 2 b? Shoulnd't we have parenthesis to make the meaning more obvious? RESPONSE:The not operator, as described in the property section is a special operator for the property, not for a boolean expression. One can optionally put parenthesis. CHANGE: Parenthesis added in the examples. Page 197: Bullet 2 says: 2) No explicit event control is allowed in any definition. Q: in which definition, and which scope does this limitation extends to? Is it the entire always block, entire property? CHANGE: The sentence changed to: "No explicit event control is allowed in any poperty or sequence declaration." Resolution of a clock for clocked sequences: Resolution of clock for a sequence definition assumes that only one explicit event control can be specified. Also, the named sequences used in the sequence definition may or may not can, but do not need to, contain event control in their definitions. It seems to me (according to the table which follows) that the resolved clock of the parent sequence is the parent sequence clock and if the sub-sequence is a sequence clock, its clock must be the identical to the parent clock. This is a better statement than providing a table based on an example. This table is ambiguous to interpret. The rules should be stated rather than illustrated with an example. RESPONSE: Perhaps, so. Although the priority of clock resolution has been already stated. No Change at the moment. Page 198: A simple statement like: if there is only one clock used in a property, this is the resolved clock. If multiple clocks are used in the a property, they must be identical and the resolved clock is that clock. If the property has no clock specified, the clock is either inferred from the always/initial clock or is the default clock visible of a clocking domain. Should replace the whole table and example. rules can be stated when the assert is a procedural assert statement inside an always or initial block (we could replace table 3 with the following rules) If both a clock property is determined and an inferred clock is determined, the inferred clock is the resolved clock. If both a default clock and a property clock is determined, the property clock is the resolved clock. If no property clock exists and there is no inferred or default clock visible, the assert statement is an illegal statement as a resolved clock must be determined. Note that the last row of table 3 is redundant with row 4 Similarly the following rules can replace table 4: For concurrent assert statements, the resolved clock is the property clock if present or the default clock if no property clock is present. RESPONSE: These are good suggestions. Given enough time, the description may be changed. No Change at the moment. Q: what happens if there is neither a property clock or a default clock? Is it an illegal statement. RESPONSE: Yes. Change: A sentence added: "All concurrent assertion statements must resolve to a clock. Otherwise, the statement is considered illegal." Q: do all these resolved clocks rules his apply to cover statement? RESPONSE: Yes. Section 17.14 Grouping assertions RESPONSE: This feature has been removed from SV3.1, and will be considered in a future version. No questions related to this feature are answered. Should not use the term parameter, it denotes something special in Verilog. Q: where can you have template declarations? It needs to be specified. Page 200: However, the replacement of a definition name is disallowed. Q: what is a definition name? I would rewrite the following sentence: The actual parameters can be given as an ordered list, as a named list. In an ordered list, the parametersare listed in the same order as in the template definition. as: In a template instantiation, the actual template arguments can be provided by position or by name. Q: where can you have template instantiations? Q does the template declaration needs to be in the same scope as the instantiation? Q: can you have a mix of name/positions? Can you have default names (like in the interfaces?) Can you skip an actual if it has a default value (like for default values in tasks/functions)? This is in fact said later page 201. Consider grouping all these rules together. My main concern is that we should have consistent rules for all constructs which allow to pass arguments by name and position. The template instance name is optional. When the name is not specified, the name is the global sequence number of the instance in the form seq_number. For example, the first template instance compiled would be assigned the name ti1. Q: why make the template instance name optional? and then requiring an automatic name being formed? What does it buy? Verilog never specified the automatic names given to unamed blocks for example. We should not do this. Page 200: A template instantiation creates a named scope. It is a named scope only if it has a name. Should write: A template instantiation with an explicit instance name created a named scope. Page 200: the example How did the posedge clk2 got transformed to $rose(clk2)? What is the difference between $rose and posedge? If no difference, why adding a systemtask? Bottom of page 200: If the default parameter value is not declared in the template definition, omission of the corresponding actual parameter value in the template instantiation will result in an error. Q: is it a compile time or runtime error? Section 17.15 Q: Where do you insert the bind directives? RESPONSE: In a module or $root. No Change Q: should the bind directives be part of the Verilog config? RESPONSE: There was no consideration of putting it as part of config. No Change Q: do you have to have a bind directive? RESPONE: No. No Change Q: Can you put assert and cover statement in a program block? RESPONSE: Yes. No Change In the following example: Example of binding to a module: bind cpu fpu_props fpu_rules_1(a,b,c); Where: — cpu is the name of module. — fpu_props is the name of the program containing properties fpu_rules_1 is the program instance name. — Ports (a, b,c) get bound to signals (a,b,c) of module cpu. — Every instance of cpu gets the properties. Example of binding to a specific instance of a module: bind cpu1 fpu_props fpu_rules_1(a,b,c); I would have thought that fpu_props was the name of a template containing a group of properties. This template could be global to the design. It is not necessary that properties are declared and belong to a program block. Some are properties of the design which can be instantiated /tested in a test program. RESPONSE: template feature has been removed. No Change Q: what about binding properties to interfaces and generate instances? Is it allowed? RESPONSE: An interface containing properties may be bound to module or instances. The functionality has been extended to interface or module instances. No Change Q: why do you have to provide a program instance to the bind directive? It seems that it should be possible to bind a set of properties to a module which has assert/cover statements of these properties. I would like a simple statement such as: bind cpu_mod template_properties It is difficult to understand how program block, properties and design code are used together. Why do we need the bind directive, isn't the program instantiation in the module itself sufficient to associate a program test with a design unit? RESPONSE: bind is provided to make it convenient for verification engineers to write properties and modify them, without touching th design files. It is also useful to attach verification IPs to modules this way. No Change