HOME

    Electronics Directory Articles/ Tutorials eBooks

About Us

FORUM Links Contact Us
   

SystemVerilog Tutorial PART 18: by Abhiram Rao

Assertions in SystemVerilog - Part1

 

 <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 that SystemVerilog assertions use. This means that the assertions, in effect, give the user 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;

 

 

 <Previous   TOC       Next >

 

Home   |    About Us   |   Articles/ Tutorials   |   Downloads   |   Feedback   |   Links   |   eBooks   |   Privacy Policy
Copyright © 2005-2007 electroSofts.com.
webmaster@electroSofts.com