Subject: [sv-ac] FW: [sv-cc] Fwd: RE: Assertion review comments up until 17.8 (included)
From: David W. Smith (david.smith@synopsys.com)
Date: Thu Apr 10 2003 - 23:00:16 PDT
Here are Francoise review comments. I have not added them to the list of
items yet (will tommorrow).
Regards
David
David W. Smith
Synopsys Scientist
Synopsys, Inc.
Synopsys Technology Park
2025 NW Cornelius Pass Road
Hillsboro, OR 97124
Voice: 503.547.6467
Main: 503.547.6000
FAX: 503.547.6906
Email: david.smith@synopsys.com
<http://www.synopsys.com/> http://www.synopsys.com
-----Original Message-----
From: owner-sv-cc@eda.org [mailto:owner-sv-cc@eda.org] On Behalf Of
Francoise Martinolle
Sent: Thursday, April 10, 2003 10:14 AM
To: fm@cadence.com; Swapnajit Mittra
Cc: sv-cc@eda.org
Subject: [sv-cc] Fwd: RE: Assertion review comments up until 17.8 (included)
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 - 22:59:39 PDT