Subject: [sv-cc] assertion review comments (second part)
From: Francoise Martinolle (fm@cadence.com)
Date: Thu Apr 10 2003 - 11:11:54 PDT
Swapnajit,
here are my review comments for the last part of the chapter 17.
Main general comment:
I think that there is a lot of work needed to clarify and polish this chapter.
After this review I am very confused on how to use
assertions/clockdomain/program blocks
and properties. I suggest that the chapter be restructured to start with
the high level concepts: the declaration of properties, how to group
properties together, how to associate properties with modules, how to
instantiate properties and execute them and finish with the details on
creating sequences.
That would help the user to grasp the methodology of property checking.
Detailed comments:
Section 17.8
typo:
The variable may be assigned any where in the sequence,
any where is one word.
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.
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.
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?
What about the value of x in the right sequence expression? is it also 0?
What about if the right sequence assigns data to x a clock tick later when
data is equal to 1:
(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).
This section needs lot of formal clarifications and needs to be
complemented with examples.
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?
$countones seems like a general purpose system function which should not be
in the
assertion chapter but in section 22.
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?
Q: can you pass actual arguments of different type than the formals?
Q: can you pass local variables as actual arguments? If yes, how do you
specify the
type of the local variable?
Q: how do you instantiate the property? Is the property declaration an
instantiation?
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.
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.
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?
Disable iff (expr) This construct clearly needs a formal description of the
logic behind it.
Some kind of a truth table should be provided.
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.
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].
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.
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.
Q: What is the use of the example of property rule1?
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?
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.
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
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.
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.
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).
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?
Section 17.12 Concurrent assertions
page 192: typo
for a sequences.
incorrrect grammar: The assert and cover statements can be referenced by
its optional name.
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
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.
Q: How and when are the results reported, accessed?
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)
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 ---)
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.
Q: what is attemptID, what is clock step? is it an integer value? Needs to
be precised.
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?
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?
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?
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?
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.
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
—
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;
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?
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?
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.
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.
Q: what happens if there is neither a property clock or a default clock? Is
it an illegal statement.
Q: do all these resolved clocks rules his apply to cover statement?
Section 17.14 Grouping assertions
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?
Q: should the bind directives be part of the Verilog config?
Q: do you have to have a bind directive?
Q: Can you put assert and cover statement in a program block?
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.
Q: what about binding properties to interfaces and generate instances?
Is it allowed?
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?
This archive was generated by hypermail 2b28 : Thu Apr 10 2003 - 11:13:57 PDT