A P P E N D I X
QUICK TUTORIAL FOR
APPENDIX A
SVA
In this appendix, we provide a quick tutorial for
SystemVerilog Assertions (SVA). It is not our objective to
present a comprehensive overview of SVA. Our goal is to
provide you with enough information so that you can
understand the examples presented in this book. For a
complete overview and reference of the SVA language, we
recommend the following sources: [Cohen 2005], [Haque et
al., 2006], and [Vijayaraghavan and Ramanathan 2005].
SVA, an assertion sublanguage of the IEEE Std 1800-2005
SystemVerilog standard [IEEE 1800-2005], is a linear-time
temporal logic that is intended to be used to specify
assertions and functional coverage properties for the
validation and verification of concurrent systems.
Using SVA, we are able to specify the design intent (that is,
expected behavior) in terms of properties. Once defined, we
can check our properties as assertions or use them as
verification constraints (assumptions), or they can describe
Appendix A, Quick Tutorial For SVA 253
behavior that must be observed during the course of
simulation (that is, coverage properties).
SVA contains two types of assertions: immediate and
concurrent. Immediate assertions follow simulation event
semantics for their execution and are executed like a
statement in a procedural block. Immediate assertions are
primarily intended to be used with simulation. In contrast,
concurrent assertions are based on clock semantics and use
sampled values of variables (that is, they exist outside the
context of procedural code).
In many respects, an immediate assertion is similar to an if
statement. They check to see if a conditional expression
holds, and if not, then the simulator generates an error
message.
For instance, Example A-1 demonstrates a portion of some
procedural code associated with an arbiter design where a
procedural statement checks that two of the arbiters
signals are never active at the same time.
Example A-1 Immediate check for mutually exclusive grants
A key observation is that the Boolean condition for the
statement is immediately checked within the procedural
context of the code (that is, when the statement is visited
during the procedural code execution).
254 Creating Assertion-Based IP
Example A-2 demonstrates the same check, except in this
case, a SystemVerilog immediate assertion is used.
Example A-2 Immediate check for mutually exclusive grants
For this example, the Boolean condition
is immediately checked only when the assert statement is
visited within the procedural context of the SystemVerilog
block. If the Boolean condition does not evaluate
true during the procedural execution of the assertion, then
an error message is automatically generated.
Immediate assertions may be used within SystemVerilog
and blocks or as a or .
There are properties of a design that must evaluate true
globally, and not just during a particular instance in which a
line of procedural code executes. Hence, SVA provides
support for concurrent assertions, which may be checked
outside the execution of a procedural block. That is, the
checks are performed concurrently with all other procedural
blocks in the verification environment.
Concurrent assertions are easily identified by observing the
presence of the SVA keyword combined with the
directive. Example A-3 situates a concurrent
assertion for our arbiter example. In this case, the concurrent
Appendix A, Quick Tutorial For SVA 255
assertion exists outside the context of a procedural always
block.
Example A-3 Immediate check for mutually exclusive grants
Concurrent assertions are based on clock semantics, use
sampled values of variables, and can be specified in always
blocks, initial blocks, or stand alone outside a procedural
block.
All of the assertion-based IP examples we present in this
book consist of a set of concurrent assertions with a specific
sample clock associated with them to prevent false firings
due to race conditions. One of the challenges associated
with immediate (unclocked) assertions contained within
procedural code is that they can suffer the same race
condition problems as other design code, which can result in
false firings during simulation. Hence, you must be careful
when using them in this context.
SystemVerilog provides a mechanism to asynchronously
disable an assertion during a reset using the SVA
clause. In Example A-4, we demonstrate the same
assertion expressed in Example A-3, except we have added
a reset signal. Even though our concurrent assertion is
clocked ( ) the assertion is asynchronously
disabled when the iff clause expression evaluates
true.
256 Creating Assertion-Based IP
.
Example A-4 Asynchronously disabling an assertion with a reset
An SVA action block specifies the actions that are taken
upon success or failure of the assertion (see the BNF
fragment in Example A-5). The statement associated with
the success of the assert statement is the first statement of an
action block. It is called the pass statement and is executed
if the expression evaluates to true. The pass statement can,
for example, record the number of successes for a coverage
log but can be omitted altogether. If the pass statement is
omitted, then no user-specified action is taken when the
assert expression holds. The statement associated with the
assertions clause is called a fail statement and is
executed if the expression evaluates to false. The fail
statement can also be omitted. The action block, if specified,
is executed immediately after the evaluation of the assert
expression.
Appendix A, Quick Tutorial For SVA 257
.
Example A-5 SystemVerilog concurrent assertion syntax
Example A-6 demonstrates an assertion where the action
blocks pass statement has been omitted, yet the fail
statement exists and is used to pass failure information out
of the assertion-based IPs analysis port.
Example A-6 SystemVerilog concurrent assertion syntax
In the previous section, we demonstrated simple assertions
based on the evaluation of a single Boolean expression that
must hold true at every sample point in time. In this section,
we introduce SVA sequences, which are Boolean
expressions that are evaluated in a linear order of increasing
time.
The temporal delay operator ## constructs sequences by
combining Boolean expressions (or smaller sequences). For
258 Creating Assertion-Based IP
instance, Example A-7 demonstrates a set of simple
sequences using the temporal delay operator.
Example A-7 Construction of sequences with temporal delay
Figure A-1 illustrates a sequence in which the Boolean
variable holds exactly one clock after holds.
Figure A-1. Trace on which the sequence (start ##1 transfer) holds
v
| | | |
start
transfer
Similarly, Figure A-2 illustrates a sequence in which the
Boolean variable holds exactly two clocks after
holds.
Figure A-2. Trace on which the sequence (start ##2 transfer) holds
v
| | | |
start
transfer
Finally, Figure A-3 illustrates a sequence in which the
Boolean variable holds between zero and two
clocks after holds. In fact, Figure A-1 and Figure A-2
also hold on the sequence defined by
.
Appendix A, Quick Tutorial For SVA 259
Figure A-3. Trace on which sequence (start ##[0:2] transfer) holds
v
| | | |
start
transfer
A temporal delay may begin a sequence. The range may be
a single constant amount or a range of time. All times may
be used to match the following sequence. The range is
interpreted as follows:
Example A-8 Construction of sequences with temporal delay
When the symbol is used, the range is infinite. For
example, specifies a sequence in which a
signal occurs at some point after a .
Assertion 6-1, A requesting client will eventually be
served on page 115 demonstrates the use of a delay
operator.
SystemVerilog provides syntactic sugar to simplify
expressing the repetition for Boolean expressions or a
sequence expression. For example, the sequence
can be expressed as sequence .
The construct is used to represent a repetition, where
is a constant. A repetition range can be expressed using
, where both and are constants.
260 Creating Assertion-Based IP
Sequence repetition examples include:
.
Example A-9 Construction of sequences with temporal delay
The first example demonstrates that a repetition of zero is
equivalent to the following:
where is any constant greater than zero.
Assertion 5-4, Valid transfer size property on page 74
demonstrates a consecutive repetition.
The goto repetition is syntactic sugar that allows for space
(absence of the term) between the repetition of the terms.
For example, a[->2] is a shortcut for the following
sequence:
Assertion 6-2, Two-client fair arbitration assertion for
client 0 on page 116 demonstrate an SVA goto repetition.
The nonconsectutive repetition operator is syntactic sugar
that allows for space (absence of a term) between the
repetition of the terms. For example, a[=2] is a shortcut for
the following sequence:
Appendix A, Quick Tutorial For SVA 261
Note the difference in the goto repetition and
nonconsecutive repetition operators. The nonconsecutive
operators do not require the repeating term to be true at the
end of the sequence. A nonconsecutive repetition is often
followed by another element in the sequence. For example:
This expression describes a sequence of two nonconsecutive
occurrences of , followed eventually by an occurrence of .
Assertion 5-11, Bus wdata properties on page 104
demonstrates a nonconsecutive repetition.
To facilitate reuse, sequences can be declared and then
referenced by name. A sequence can be declared in the
following:
a module
an interface
a program
a clocking block
a package
a compilation-unit scope
Sequences can be declared with or without parameters, as
demonstrated in Example A-10.
262 Creating Assertion-Based IP
.
Example A-10 Declared sequences
SystemVerilog allows for declarations of properties to
facilitate reuse. A property differs from a sequence in that it
contains a clock specification for the entire property and an
optional asynchronous term to disable the property
evaluations.
Named properties can be used to construct more complex
properties, or they can be directly used during verification
as an assertion, assumption, or coverage item. Properties
can be declared with or without parameters, as demonstrated
in Example A-11.
.
Example A-11 Declared properties
Properties may reference other properties in their definition.
They may even reference themselves recursively. Properties
Appendix A, Quick Tutorial For SVA 263
may also be written using multiple clocks to define a
sequence that transitions from one clock to another as it
matches the elements of the sequence.
The sequence operators defined for SystemVerilog allow us
to compose expressions into temporal sequences. These
sequences are the building blocks of properties and
concurrent assertions. The first four allow us to construct
sequences, while the remaining operators allow us to
perform operations on a sequence as well as compose a
complex sequence from simpler sequences.
Both SVA properties and sequences can be operands of the
and operator. The operation on two sequences produces a
match when both sequences produce a match (the end point
may not match). A match occurs until the endpoint of the
longer sequence (provided the shorter sequence produces
one match).
Examples of sequence and are:
.
Example A-12 Sequence AND
264 Creating Assertion-Based IP
An intersection of two sequences is like an and of two
sequences (both sequences produce a match). This operator
also requires the length of the sequences to match. That is,
the match point of both sequences must be the same time.
With multiple matches of each sequence, a match occurs
each time both sequences produce a match.
Example A-13 demonstrates the SVA sequence intersect
operator.
.
Example A-13 Sequence intersect
SVA provides a means to or sequences. For or-ed
sequences, a match on either sequence results in a match for
the operation
Example A-14 demonstrates the SVA sequence or operator.
.
Example A-14 Sequence OR
Appendix A, Quick Tutorial For SVA 265
This operator is used to specify a Boolean value throughout
a sequence. The operator produces a match if the sequence
matches and the Boolean expression holds until the end of
the sequence.
Example A-15 demonstrates the SVA sequence throughout
operator.
.
Example A-15 Sequence throughout
The within operator determines if one sequence matches within
the length of another sequence.
Example A-16 demonstrates the SVA sequence within
operator.
.
Example A-16 Sequence within
266 Creating Assertion-Based IP
The method ended returns true at the end of the sequence.
This is in contrast to matching a sequence from the
beginning time point, which is obtained when we use only
the sequence name.
Example A-17 demonstrates the SVA sequence ended
method.
.
Example A-17 Sequence ended
The first_match operator returns true only for the first
occurrence of a multiple occurrence match for a sequence.
Example A-18 demonstrates the SVA sequence first_match
method.
.
Example A-18 Sequence ended
Appendix A, Quick Tutorial For SVA 267
SystemVerilog supports implication of properties and
sequences. The left-hand operand of the implication is
called the antecedent and the right-hand operand is called
the consequent. Evaluation of an implication starts through
repeated attempts to evaluate the antecedent. When the
antecedent succeeds, the consequent is required to succeed
for the property to hold.
As a convenience, there are two forms of implication,
overlapping ( ) and non-overlapping ( ). The overlap
occurs between the final cycle of the left-hand side (the
antecedent) and the starting cycle of the right-hand side (the
consequent) operands. For the overlapping form, the
consequent starts on the current cycle (that the antecedent
matched). The non-overlapping form has the consequent
start the subsequent cycle. Implication is similar in concept
to an if statement.
Example A-19 demonstrates the SVA implication operators.
.
Example A-19 Implication operators
SVA provides various system functions to facilitate
specifying common functionality. This section describes a
few of SVAs more commonly used system functions.
268 Creating Assertion-Based IP
Sampled value functions include the capability to access the
current or past sampled value, or detect changes in the
sampled value of an expression. The following functions are
provided:
Using these functions is not limited to assertion features;
they can be used as expressions in procedural code as well.
The clocking event, although optional as an explicit
argument to the functions, is required for semantics. The
clocking event is used to sample the value of the argument
expression.
The clocking event must be explicitly specified as an
argument or inferred from the code where it is used. The
following rules are used to infer the clocking event:
If used in an assertion, the appropriate clocking event
from the assertion is used.
If used in an action block of a singly clocked assertion,
the clock of the assertion is used.
If used in a procedural block, the inferred clock, if any,
for the procedural code is used.
Otherwise, default clocking is used.
In addition to accessing value changes, the past values can
be accessed with the $past function. The following three
optional arguments are provided:
expression2 is used as a gating expression for the
clocking event
Appendix A, Quick Tutorial For SVA 269
number_of_ticks specifies the number of clock ticks in
the past
clocking_event specifies the clocking event for
sampling expression1
The expression1 and expression2 can be any expression
allowed in assertions.
Assertion 5-12, Bus slave ready assertions on page 105
demonstrates both a and . Assertion 5-5, Bus
must reset to INACTIVE state property on page 86
demonstrates .
Assertions are commonly used to evaluate certain specific
characteristics of a design implementation, such as whether
a particular signal is one-hot. The following system
functions are included to facilitate such common assertion
functionality:
$onehot (<expression>) returns true if only one bit of
the expression is high.
$onehot0 (<expression>) returns true if at most one bit
of the expression is high.
$isunknown (<expression>) returns true if any bit of
the expression is X or Z. This is equivalent to
^<expression> bx.
All of the above system functions have a return type of bit.
A return value of 1b1 indicates true, and a return value of
1b0 indicates false.
Another useful function provided for the Boolean
expression is $countones, to count the number of ones in a
bit vector expression.
$countones ( expression)
270 Creating Assertion-Based IP
An X and Z value of a bit is not counted towards the number
of ones.
Assertion 6-6, Built-in function to check mutually
exclusive grants on page 119 demonstrates a $onehot
system function.
SystemVerilog has defined several severity system tasks for
use in reporting messages. These system tasks are defined as
follows:
$fatal(finish_num [, message {, message_argument } ] );
This system task reports the error message provided and
terminates the simulation with the error code.
This system task is best used to report fatal errors related to
testbench/OS system failures (for example, cant open, read,
or write to files) The message and argument format are the
same as the $display() system task.
$error( message {, message_argument } );
This system task reports the error message as a run-time
error in a tool-specific manner. However, it provides the
following information:
severity of the message
file and line number of the system task call
hierarchical name of the scope or assertion or property
simulation time of the failure
$warning(message {, message_argument } );
This system task reports the warning message as a run-time
warning in a format similar to $error and with similar
information.
Appendix A, Quick Tutorial For SVA 271
$info(message {, message_argument } );
This system task reports the informational message in a
format similar to $error and with similar information.
$asserton(levels, [ list_of_modules_or_assertions])
This system task will reenable assertion and coverage
statements. This allows sequences and properties to match
elements. If a of 0 is given, all statements in the
design are affected. If a list of modules is given, then that
module and modules instantiated to a depth of the
parameter are affected. If specifically named assertion
statements are listed, then they are affected.
$assertkill(levels, [ list_of_modules_or_assertions])
This system task stops the execution of all assertion and
cover statements. These statements will not begin matching
until re-enabled with $asserton(). Use the arguments in the
same way as $asserton uses them.
$assertoff(levels, [ list_of_modules_or_assertions])
This system task prevents matching of assertion and cover
statements. Sequences and properties in the process of
matching sequences will continue. Assertion and cover
statements will not begin matching again until re-enabled
with $asserton(). Use the arguments in the same way as
$asserton uses them.
SVA includes the ability to call a routine or sample data
within the sequence for later analysis. The ability to call a
routine (tasks, void functions, methods, and system tasks)
allows you to record data for analysis or debugging.
Example A-20 demonstrates the SVA sequences with
system task calls.
272 Creating Assertion-Based IP
.
Example A-20 Calling system task within a sequence
SVA sequences allow you to declare local variables that can
be used to sample data at a specific point within a sequence.
Example 5-12, Encapsulate coverage properties inside a
module on page 111 demonstrates an SVA sequence with a
local variable. Long et. al [2007] provide an excellent
overview and set of guidelines for coding local variables.
SVA directives specify how properties are to be used.
Example A-21 describes the syntax for SVA directives.
.
Example A-21 Directives
Appendix A, Quick Tutorial For SVA 273
This section defines a set of useful, named property
declarations we have created with the intent to be shared by
an assertion-based IP design team. Our goal is to create a set
of named properties that is similar to a some of the
expressive IEEE 1850 Std. Property Specification Language
(PSL) [IEEE 1850-2005] linear-time temporal operators.
This allows us to express complex properties with minimum
code through reuse.
.
Example A-22 Named property declarations
274 Creating Assertion-Based IP
