Subject: [sv-cc] Fwd: RE: Assertion review comments up until 17.8 (included)
From: Francoise Martinolle (fm@cadence.com)
Date: Thu Apr 10 2003 - 10:13:33 PDT
Swapnajit,
please find my review comments on chapter 17 up until section 17.8
I will send you the comments for the rest later today
>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.
>
>$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.
>
>
>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?
>
>
>Section 17.4:
>Q: there is no bnf for concurrent assertions, are they the same as the
>immediate assertions but are
>concurrent?
>
>
>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.
>
>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".
>Q: Why requiring to specify 0? why not allowing " a b" instead of a ##0 b?
>
>
>"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
>
>
>
>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.
>
>Page 166: example does not match explanation.
>req ##22 gnt
>
>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.
>
>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.
>
>
>
>
>
>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.
>
>I am also assuming that we are declaring seq1 to be a ##1 b ##1 c. This is
>not shown in the example.
>
>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
>
>Q: Isn't the above also equivalent to:
>a ##1 b ##1 c ##0 d ##1 e ##1 f
>
>
>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
>
>Section 17.6 page 168:
>a name that is not a definition name
>
>Q: What is a definition name?
>
>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?
>
>"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.
>
>page 170:
>typo:
>which which means
>
>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
>
>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.
>
>Section 17.7.2:
>$rose, $fell, $stable
>Q: why are these past tense rather than $rise, $fall?
>Section 17.7.3:
>I have the same remark as the editor. Why not using &?
>
>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.
>
>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.
>
>
>
>I don't understand what the note means:
>Note that first_match applies to each attempt for the sequence individually.
>
>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).
>
>
>
>
>
>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.
>
>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.
>
>Section 17.7.10:
>Q: why using a method rather than a system task $end?
>
>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.
>
>Page 183: typo
>Each time a data phase completes, a match for data_end is recognized. The
>Should be data_phase.
>
>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?
>Q: Why are we using a macro instead of a sequence declaration?
>
>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.
>
>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.
>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 &&.
>
>
>
>
>
>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.
>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.
>
>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.
>
>Page 186 in Bullet 3, there is a mistmatch use of "&&" and "and"
>Q: Which one is correct?
>The description is quite confusing. There is no definition of what is the
>symmetry difference.
>
>Q: What is the effect of assigning a value of data to x and reading x in
>another sequence?
>Q: Which value would I get for x?
>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?
>
>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.
This archive was generated by hypermail 2b28 : Thu Apr 10 2003 - 10:18:34 PDT