|
<Previous
TOC
Next >
SystemVerilog Assertions Benefits:
SystemVerilog built
assertions directly into the design and verification language, and that
provides clear benefits. In fact, SystemVerilog has effectively unified
assertions with the design and verification language for use in both
simulation and formal verification. The key benefits of SVA can be
summarized as follows:
� Ease of adoption because it
is built on a familiar language and syntax
� Less assertion code due to
automatic contextual understanding of design control logic
� Simple hookup and
interaction between assertions and the testbench without special
interfaces
� Customization and control
of messaging and error severity levels
� Ability to interact with
Verilog and C functions
� Avoidance of mismatching
results between simulation and formal evaluations with clearly defined
scheduling semantics
� Ability to improve
verification performance by eliminating assertion co-simulation overhead
and reusing simulation optimization algorithms
These benefits will be described in the following
sections.
SystemVerilog Assertions Overview
SystemVerilog assertions were
developed to provide design and verification engineers the means to
describe complex behaviors about their designs in a clear and concise
manner, building on concepts with which users are already familiar. With
SVA unified syntactically with the rest of SystemVerilog, the user is able
to embed assertions directly in-line with the design and other
verification code, allowing the tools to infer a great deal of information
from the context of the surrounding code. This reduces, in many cases
substantially, the amount of code the user must write to specify the
behavior, and simplifies the usage model since this information does not
have to be duplicated, as it would with a separate assertion language.
The semantics of SVA are
defined such that the evaluation of the assertions is guaranteed to be
equivalent between simulation, which is event-based, and formal
verification, which is cycle-based. This equivalence ensures that multiple
tools will all interpret the behaviors specified in SVA in the same way.
Moreover, the unification of assertions with design and verification code
streamlines interaction to augment the power of assertions. In particular,
SystemVerilog allows assertions to communicate information to the
testbench and allows the testbench to react to the status of assertions
without requiring a separate application programming interface (API) of
any kind.
SystemVerilog provides two
types of assertions: immediate and concurrent.
Both assertion types are intended to convey the intent of the design
engineer and to identify the source of a problem as quickly and directly
as possible. Immediate assertions are procedural statements that can occur
anywhere within always or initial blocks, and include a
conditional expression to be tested and a set of statements to be executed
depending on the result of the expression evaluation.
The syntax of an immediate
assertion is shown here:
|
immediate_assert_statement ::=
assert ( expression
) [[ pass_stmt ] else fail_stmt ]1. |
The expression is evaluated
immediately when the statement is executed, exactly as it would be for an
if statement. The pass_stmt is executed if the expression evaluates
to true, otherwise the fail_stmt is executed. The pass and fail
statements, if present, are executed immediately after the expression is
evaluated. Because an assertion carries with it the implication that the
expression will be true, the failure of an assertion has a severity
associated with it. SystemVerilog includes four system tasks ($fatal,
$error, $warning and $info) that can be included in the fail statement
block to indicate the severity of the failure and print additional
user-defined debug messages, if desired. This is roughly the same
functionality as the VHDL assert statement.
Concurrent Assertions
The real power of SVA, both
for simulation and formal verification, is the ability to specify behavior
over time, which VHDL assertions cannot do. Concurrent assertions provide
the ability to specify such sequential behavior concisely and to evaluate
that behavior at discrete points in time, usually clock ticks (e.g.
�posedge clk�). The concepts and components that make up concurrent
assertions can best be understood as a set of layers, each building on the
layer(s) below:
The basic function of an
assertion is to specify a set of behaviors that is expected to hold true
for a given design or component. The Boolean expressions layer is the most
basic, and specifies the values of elements at a particular point in time,
while the sequential regular expressions layer builds on the Boolean layer
to specify the temporal relationship between elements over a period of
time. The property declarations layer builds on sequences to specify the
actual behaviors of interest, and the assertion directives layer
explicitly associates these behaviors with the design and guides
verification tools about how to use them.
Sampling
To ensure consistency between
simulation and formal verification tools, which apply a cycle-based view
of the design, concurrent assertions in SystemVerilog use sampled values
of signals to evaluate expressions. The sampled value of signals is
defined to be the value of the signal at the end (i.e. at read-only
synchronization time as defined by the PLI2 ) of the last simulation time
step before the clock occurs. This way, a predictable result can be
obtained from the evaluation, regardless of the simulator�s internal
mechanism of ordering and evaluating events.
This explicit notion of
sampling signals relative to a clock edge is an integral part of the
behavior of SystemVerilog assertions and is made possible in part because
the assertions are simply another part of the SystemVerilog language. The
existing Verilog scheduling mechanism has been extended to support value
sampling and to provide �hooks� for the assertions to work seamlessly with
the rest of the language. These scheduling extensions allow simulators and
other tools to apply existing optimization algorithms to the execution of
assertions as well as the modeling of the design and the testbench.
Separate assertion languages
cannot define this explicit sampling mechanism because the required hooks
are not part of Verilog. The behavior can be approximated in Verilog in
some cases if the user adheres to a restricted coding style. But the
possibility of race conditions and multi-clock systems makes it impossible
to guarantee consistency between formal verification and simulation tools
in all cases, without specifically enhancing the Verilog scheduling
explicitly to support this particular goal.
Race conditions are an
artifact of the event-based scheduling semantics of Verilog, which allow
multiple events to occur at a given simulation time. Since synthesis and
formal verification tools take a cycle-based view of the design, race
conditions are always resolved according to the same sampling semantics
���) V ���) V �Q�) V �V�) V ���) V ���) V �8 ���) V r a post-synthesis view of the design during
pre-synthesis RTL verification, eliminating pre- and post-synthesis
mismatches.
Concurrent assertions differ
from immediate assertions in two important ways. First, in addition to
being instantiated procedurally in a design as a statement in an
always or initial block, concurrent assertions can also be
instantiated declaratively as a module-level statement (similar to
a continuous assignment) outside of procedural blocks. The second
difference is that concurrent assertions allow the specification of a
temporal behavior to be checked, instead of just a combinational condition
as immediate assertions do.
The syntax of a concurrent
assertion is:
|
concurrent_assert_statement ::=
assert property ( sequential_expr_or_property
)
[[ pass_stmt ] else fail_stmt ] |
The sequential expression is
evaluated using sampled values of the signals, and the pass/fail
statements allow the assertion to communicate with the testbench. Because
the assertions are an integral part of the language, these statements can
use the full breadth of SystemVerilog to trigger events, record coverage
information or otherwise affect the flow of the verification code,
including calling C code. Separate assertion languages are effectively
�read-only� in that they can only monitor design behavior but cannot
affect elements in either the design or the testbench.
Immediate assertions
The immediate assertion
statement is a test of an expression performed when the statement is
executed in the procedural code. The expression is non-temporal and is
interpreted the same way as an expression in the condition of a procedural
if statement. That is, if the expression evaluates to X, Z or 0,
then it is interpreted as being false and the assertion is said to fail.
Otherwise, the expression is interpreted as being true and the assertion
is said to pass.
The immediate assert
statement is a statement_item and can be specified anywhere a
procedural statement is specified.
|
procedural_assertion_statement::=
...
immediate_assert_statement
immediate_assert_statement ::=
assert ( expression
)
action_block
action_block ::=
statement_or_null
[
statement ]
else
statement
|
The action_block
specifies what actions are taken upon success or failure of the
assertion. The statement associated with the success of the assert
statement is the first statement. 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 is true. The
statement associated with else is called a fail statement
and is executed if the expression evaluates to false. The else
statement can also be omitted. The action block is executed immediately
after the evaluation of the assert expression.
The optional statement label
(identifier and colon) creates a named block around the assertion
statement (or any other SystemVerilog statement) and can be displayed
using the %m format specification.
assert_foo : assert(foo)
$display("%m passed");
else
$display("%m failed");
Since the assertion is a
statement that something must be true, the failure of an assertion shall
have a severity associated with it. By default, the severity of an
assertion failure is error. Other severity levels can be specified
by including one of the following severity system tasks in the fail
statement:
-
$fatal is a run-time fatal.
-
$error is a run-time error.
-
$warning is a run-time
warning, which can be suppressed in a tool-specific manner.
-
$info indicates that the
assertion failure carries no specific severity.
If an assertion fails
and no else
clause is specified, the tool shall, by default, call $error, unless a
tool-specific option, such as a command-line option, is enabled to
suppress the failure.
All of these severity system
tasks shall print a tool-specific message indicating the severity of the
failure, and specific information about the specific failure, which shall
include the following information:
-
The file name and line
number of the assertion statement.
-
The hierarchical name of
the assertion, if it is labeled, or the scope of the assertion if it is
not labeled.
For simulation tools, these
tasks shall also include the simulation run-time at which the severity
system task is called. Each system task can also include additional
user-specified information using the same format as the Verilog
$display.
If more than one of these
system tasks is included in the else clause, then each shall be
executed as specified. If the severity system task is executed at a time
other than when the assertion fails, the actual failure time of the
assertion can be recorded and displayed programmatically. For example:
|
time t;
always @(posedge clk)
if (state == REQ)
assert (req1 || req2)
else begin
t = $time;
#5 $error("assert failed at time %0t",t);
end |
If the assertion fails at
time 10, the error message shall be printed at time 15, but the
user-defined string printed shall be �assert failed at time 10�.
The display of messages of
warning and info types can be controlled by a tool-specific option, such
as a command- line option.
Since the fail statement,
like the pass statement, is any legal SystemVerilog procedural statement,
it can also be used to signal a failure to another part of the testbench.
|
assert (myfunc(a,b)) count1 = count + 1; else
->event1;
assert (y == 0) else flag = 1; |
|
