Saving Time and Increasing Design Accuracy with System Verilog Assertions

System Verilog Assertions (SVA) integrate well with UVM testbenches and make verification easier and more accurate. Steps can be taken to reduce coding overhead and allow for greater flexibility for reuse. While not all requirements are ideal for assertions, this paper aims to explain that, when used correctly, SVA can save time and increase design accuracy.

What are Assertions?

Assertions are expressions that define a condition for a signal or combination of signals in the design under test (DUT). They either pass or fail and allow the author to define when the condition is evaluated. In the most basic version of an assertion the clock is inferred from the encompassing always block and is evaluated once per clock cycle. The example below generates an error if signal is not equal to zero at the active clock edge.

signal_low: assert property(signal == 0);

More complex assertions can be utilized. For example, timing information and conditions can be defined separately in sequences and properties. This is useful for reuse allowing a timing sequence to be used in multiple properties or a property to be applied to multiple DUT signals.

sequence signal_low_s(a);
    (a == 0);
endsequence

property signal_low_p;
    @(posedge clk) signal_low_s(signal);
endproperty

signal_low: assert property (signal_low_p);

There is more complex syntax, and a library of options an engineer can use for verifying requirements, although those are beyond the scope of this paper.

Who should write assertions?

Assertions are valuable for verification engineers and are not just for designers. While they are good for checking simple things while designing blocks, they have value in more complex forms to be used by verification engineers as part of top level testbenches.

Some verification efforts can be completed using exclusively assertions taking advantage of the tools assertions provide to verify complex behavior. Techniques for using assertions to enhance a UVM based testbench are described below.

What type of requirements are ideal for assertions?

In UVM based testbenches, there can be observability issues when trying to test critical pieces of a design. Many requirements are generated to specify behavior that takes place within a module. Detecting a bug in a UVM testbench requires that it is triggered through the testbench interface and evidence of the bug must be visible at the output interface.

Fault handling modules and their associated requirements are examples of potential bugs that violate requirements but are only visible internally. A requirement may specify an error condition that must be detected within the module and corrected internally. Requirements that concern what types of errors and the timing for when an error must be corrected inside the module may not be visible at the output interface. Adding an assertion to target a specific internal module signal can ensure a bug is detected for behavior that is not visible at the top level scoreboard.

Guidelines for Verification Engineers

Link assertions to design requirements

Each assertion needs to have a clear link to the requirement it was written about. This can be tracked in the requirements document or automated with verification tools.

Write assertions from a black box perspective when possible

Black box style assertions can save the author from rewrites in the event that DUT code changes.

One example is an assertion checking data throughput. A black box assertion compares input and output data rate. An example of a problem with a whitebox assertion would be a check that a FIFO full flag goes high at the appropriate time to show throughput is correct given the FIFO size. The designer could change how the FIFO works or remove it entirely resulting in a rewrite by the verification engineer.

Write properties as generally as possible to promote reusability

Assertions can be used with arguments to be reused across many signals in the design.

Use assertions to identify pass/fail criteria for tests

Assertions generate an error if an illegal condition in the DUT occurs during a test run. This is a simple way to cause a test to fail if an illegal condition occurs.

Write assertions in a bind file to create the connection to DUT modules

Bind files allow assertions to have full access to all the signals in a DUT without modifying any of the code.

All module inputs and outputs are easily connected, followed by any required internal signals. It is important to document when and why internal signals are needed.

Basic bind example:

bind my_dut my_assertion_module my_assertion_inst 
    (.clk(clk), 
     .signal(signal));

Techniques for Assertion Reuse

Many top-level requirements are similar from project to project. Properties allow verification engineers to define conditions with arguments. This allows many properties to be reused for common high-level assertions. Reusing assertions allows engineers to spend time on the unique aspects of a design. Properties also help with consistency across a testbench. One engineer can write properties that can be used in all blocks of a testbench allowing certain requirements that are repeated to be checked uniformly across the design.

Sequences and properties can have arguments passed in to reduce overhead coding. This allows engineers to focus on writing Boolean expressions to test requirements. The example below applies the conditional expression to 3 different DUT signals without having to repeat lines.

property signal_low_p(bit my_signal);
    @(posedge clk) (my_signal==0);
endproperty

signal_1_low: assert property (signal_low_p(signal_1));
signal_2_low: assert property (signal_low_p(signal_2));
signal_3_low: assert property (signal_low_p(signal_3));

Generate statements can be used to create a large number of repeated assertions that apply to similar signals across the design. The example below checks each bit of signal separately.

generate
    for(int i = 0; i<10; i++) begin
        signal_low: assert property(signal[i] == 0);
    end
endgenerate

Code Review

Reviewing testbench changes in UVM is time consuming and requires looking at multiple files, while assertions tend to be more succinct. Assertions contain all the information needed to check if new code accomplishes its intended purpose.

When an engineer reviews a new test, the files that must be reviewed include the test, any new sequences used in the test, and the scoreboard checking the behavior. Files that have not been modified are also needed to provide context for the proposed change. By contrast, to review an assertion, the reviewer can simply check how the DUT signals are being compared in the assertion to determine if it matches the requirement.

signal_low_req101: assert property(signal == 0);

To review the assertion above, the reviewer does not need any information from the author. The versioning tool will indicate what line has changed, and the assertion label indicates the requirement in question. The subject of the assertion, signal, can be traced back to the DUT through the bind file.

Advantages of using SVA with UVM

An advantage of assertions is that they can be turned off, and the testbench can be run without them. The bind file allows the assertions to be non-invasively integrated with the DUT and testbench.

Metrics are simplified when writing assertions. Tools collect pass/fail data for all assertions in a design and are easily linked to functional coverage for signoff artifacts. The action blocks can be used to provide detailed error information, and the assertion label can also provide context.

Counters can be used to set a minimum threshold for how many times an assertion must pass. Assertions also provide a clear mechanism for enabling them to run only during valid portions of a test.

A simple way to disable assertions during specific conditions is by using disable iff:

signal_low_req101: 
    assert property(disable iff(reset==1) signal == 0);

The condition inside the disable iff statement allows the user to control whether the assertion is evaluated.

Conclusion

Integrating SVA into your UVM testbench with the proper planning and structure can save time and help verify unique requirements that otherwise might lead to undiscovered bugs. Coding guidelines can be implemented to ensure easy reuse and simple code review. Understanding the power of assertions can save time and complexity when attempting to cover requirements that are not as visible from the top level or require complex timing checks.