Importance of Assertion Based Verification

Introduction

The increase in the complexity of chip designs has led to an increase in the time taken to complete the verification of a design. Verification is done to ensure that the design of the chip meets all the requirements as specified by the specifications document. To this end, design verification implements checkers to check the behavior of the design. To aid the implementation of the checkers, System Verilog provides assertions. Assertion is a powerful feature which can speed up the design verification process.

Assertion is a signal level checker which can be used both by the designer and verification engineer. Let us deep dive into assertion and its importance.

What is Assertion?

Assertion can be viewed as an instruction to the verification tool. It validates the behavior of the design and is used to check design rules or specifications are covered in the verification.  The main functionality of the assertion checker is that it implicitly throws an error when the checker fails, that is, design’s behaviour is not as per the specification. The behavior which needs to be checked can be captured using the property and sequence constructs available in System Verilog. 

By default, there are no display statements when assertion passes. But we can customize to have a print statement when the assertion passes or fails. The severity of the message when the assertion fails can be customized to any type – info, warning, error or even fatal message. 

The syntax for using assertions is as follows.

Syntax:        

assert(C==D);     //only throws error when C is not equal to D
                  //assert is a keyword used while defining the assertion

assert(C==D)  $display(“Pass statement”);
                     // prints pass statement when C == D, that is, assertion passes
else $error(“Fail statement”);
                     // prints fail statement when C is not equal to D, that is, assertion fails

Types of assertion:

There are 2 types of assertions.

1. Immediate assertion

2. Concurrent assertion

Immediate assertion:

Immediate assertion is a procedural statement which checks whether a condition or expression is true or not, if the given expression is not true an error will be thrown. It is like an if condition, but an error is thrown automatically whenever the condition fails. This type of assertion can be only used inside procedural blocks like initial, always, methods, etc.

//Syntax for if condition check:
if(X==Y)  
  $display(“PASS statement”);
else 
  $display(“FAIL statement”);

//Syntax for immediate assertion:
assert(X==Y);

Concurrent Assertion:

Concurrent assertion is like immediate assertion, but it checks the condition periodically throughout the simulation. Concurrent assertions are based on a clocking event which acts as a trigger to check the expected behavior. The clock acts as the clocking event for the concurrent assertion.  Concurrent assertion is implemented using property and sequence.

//Syntax for concurrent assertions:
eq_assert: assert property (@(posedge clk) C==D);
//eq_assert : Label name given for assertion.
//assert, property: keywords provided by System Verilog.
//@(posedge clk)  : acts as clocking event, that is, trigger.

Property and Sequences:

Properties and sequences act as building blocks for concurrent assertion. Property is used to capture the expected behavior. Sequence is a procedural statement which needs to be true. A single property can call multiple sequences. Sequence enables reusability in multiple property.

Syntax:

property property_name;
      // seq can be called 
endproperty
assert property (property_name);

sequence  seq_name; 
     //expression to be checked 
endsequence

The above example,

eq_assert: assert property (@(posedge clk) C==D);

can be written using property and sequence as follows.

sequence eq_seq;
      C==D;
endsequence

property eq_prop;
@(posedge clk) eq_seq;
endproperty

eq_assert: assert_property(eq_prop);

There are many inbuilt constructs/system tasks available in system Verilog which can be used in property to implement the expected behavior. Some of them are listed below 

• Disable iff: To disable the assertion based on some conditions.

• Temporal operator: To describe the behavior of a signal over time in the assertion check. 

• Implication operator: To check consequent expression if antecedent expression satisfied.

• $rose: To detect the signal transition from low to high.

• $fell: To detect the signal transition from high to low.

• $stable: To detect whether the value of the signal remains the same between two adjacent events.

• $past: To check the value of the signal in previous clocking events.

Why is assertion-based verification useful?

Assertion based verification has many advantages. 

• It saves time during the verification process because assertion checkers are easy to implement. 

• It is a quicker method to identify the bugs in a design. Assertion failures pinpoint the exact time when a particular issue occurred. This eases the debugging process. 

• Assertions can also be used to implement coverage with the help of the keyword “cover”

• With the help of the keyword “assume” assertions can be used for formal verification as well. 

• Assertions can be turned ON/OFF based on the need. 

• Assertion checkers can be used in different levels of verification, that is, SOC level, subsystem level and IP level. 

• Assertion checkers can also be viewed in waveform. All simulators provide assertion browsers to check the activity and status of the assertion checkers implemented. This is a great advantage and helps in shortening the debugging time.

Summary

As we seen above, implementation of assertion-based verification saves time, and it is simple and effective. Assertion based verification is an IEEE standard as well. It can be used in both dynamic simulation and formal verification. One must remember that though assertion-based verification provides a lot of advantages, there are some cases like data conversion checker which can be easily implemented by conventional checker with the help of scoreboard. So, depending on the type of verification required, we can choose between scoreboard-based checkers and assertions.