What are SystemVerilog Assertions?
With a lot of increase in design complexity, the effort required to verify these designs is also increasing at a faster rate. To improve the verification quality we use various methods, techniques and SystemVerilog Assertions are one important feature we use to verify the design.
But do you know what are SystemVerilog Assertions?
SystemVerilog Assertions are a piece of verification code, which checks the design in adherence to the specification which will validate the specific behavior of a design and displays a message. If the specified behavior is not exhibited by the design then the assertion fails, indicating an error in the design’s behavior.
Assertions can be checked dynamically by simulation, or statically by formal verification EDA tool that proves whether the design meets its specification requirement or not. These tools require specifications about the design’s behavior.
Assertions can provide two major information about the design,
- Is the design working correctly?
- How good the test case is?
SystemVerilog Assertions can also provide coverage information which makes sure a certain design specification is covered in the verification. The concept/methodology of using assertions to verify a design is called Assertion based Verification – ABV.
Also read: SystemVerilog Event Scheduler
Advantages of using SystemVerilog Assertions
- Assertions improve the observability and controllability of the design.
- Observability – the ability to observe the effects of a specific, internal state, data path within the design.
- Controllability – the ability to activate, stimulate, or sensitize a specific point within the design.
- Assertions improve debugging of the design.
- It helps to capture the bugs which do not propagate to the output.
- Assertions can find the source of the bug faster and more accurately.
- It helps to capture the improper functionality of the design at or near the source of the problem thereby reducing the debug time.
- Assertions give white box visibility to the design by providing internal test points in the design.
- Simplifying the diagnosis and detection of bugs by localizing the occurrence of a suspected bug to an assertion monitor, which is then checked.
- Assertions check design specifications and report errors or warnings in case of failure.
- Assertions can be re-used across a design at various levels of verification.
- Assertions can be parameterized so they could be reused.
- Assertions can be turned on/off based on the requirement.
- Ability to interact with C and Verilog functions.
Who writes SystemVerilog Assertions?
SystemVerilog Assertions can be written in the design as well as in the verification environment.
Design Engineers – White box verification
- For the Signals at the Micro Architecture level (for the signals which are not visible to Verification Engineers)
Verification Engineers – Black box verification
- For the I/O signals of IP or SoC.
What are the challenges with SystemVerilog Assertions?
- The quality of the test stimulus is still critical.
- Assertions are only useful if exercised by the test stimulus.
- Assertions must be defined carefully.
- Incorrect assertions can give misleading results.
- Debugging an assertion can be difficult.
- How do we know when enough assertions have been written?
- Simulation overhead.
Also read: What is the use of SystemVerilog assertion?
Types of SystemVerilog Assertions
- Immediate assertions
- Concurrent assertions
An assertion that checks a condition at the current simulation time is called an immediate assertion. Immediate assertions are procedural statements that can check only a combinational condition are evaluated immediately and they cannot involve any temporal operators.
|Syntax: assert (condition_to_be_checked);|
Example: Immediate Assertion
|wire #1 reset_delay = reset;
always @(posedge reset_delay)
begin : dff_chk
rst_check : assert (q == 0)
$display(“The reset check is failed at time t = %0d”,$time);
end : dff_chk
As immediate assertions are instantaneously checked, they may report false failures due to multiple input changes at the same time. These unexpected multiple executions need to be avoided.
An extension to the immediate assertion is deferred immediate assertion and is used to avoid the multiple outputs or errors created due to the unexpected glitching activity on inputs in the immediate assertions.
Concurrent assertions periodically sample the test signals and are based on clock edges. Concurrent assertion is the most valuable assertion style that can be used in design and verification environments. The concurrent assertions are executed in a three-step process, i.e sampling the values, evaluating the test condition and executing the report in the below regions,
- Preponed region – In this region, the values for the assertion variables are sampled. In this region, a net or variable cannot change its state. This allows the sampling of the most stable value at the beginning of the time slot.
- Observed region- All the property expressions are evaluated in this region.
- Reactive region- The pass/fail code (Action blocks) from the evaluation of the properties are scheduled in this region.
Example: concurrent assertion
@(posedge clk) disable iff (rst)
t |=> q == !($past(q,1));
toggle_check : assert property (t_in)
$display(“The toggle check is failed at time t = %0d”,$time);
Case Study: AHB
Let us see some example assertions on AHB protocol.
- Assertion to check write data and address during busy transfer.
|//Busy – Address and Write Data
@(posedge Hclk disable iff(!Hresetn)
((Htrans == 1) && (Hwrite)) |=> ((Htrans != 0) && (Haddr == $past(Haddr, 1)));
addr_busy_check : assert property (write_busy)
- Assertion to check address for burst transfer wrap4 with halfword.
|//Address – WRAP4 Halfword
@(posedge Hclk) disable iff(!Hresetn)
(Htrans == 3) && (Hburst == 2) && (Hsize == 1) && ($past(Htrans, 1) != 1) && ($past(Hready, 1)) |-> ((Haddr[2:1] == ($past(Haddr[2:1], 1) + 1)) && (Haddr[31:3] == $past(Haddr[31:3], 1)));
wrap4_size1_addr_check : assert property (addr_wrap4_size1)
- Assertion to check the boundary alignment for Word
|//Address – Boundary Alignment for Word
@(posedge Hclk) disable iff(!Hresetn)
Hsize == 2 |-> Haddr[1:0] == 0;
size2_addr_check : assert property (addr_Hsize2)
- Assertion to check address for incremental burst.
|//Address – Incremental burst
@(posedge Hclk) disable iff(!Hresetn)
(Htrans == 3) && ((Hburst == 1)||(Hburst == 3)||(Hburst == 5)||(Hburst == 7)) && ($past(Htrans, 1) != 1) && ($past(Hready, 1)) |-> (Haddr == ($past(Haddr, 1) + 2**Hsize));
incr_check : assert property (incr_addr)
Also read: How do I learn SystemVerilog in a week?
In assertion-based verification, the assertions are used to capture design intent in a verifiable form providing a mechanism to check for correct behavior. During simulation, assertions improve controllability and observability, making the source of an error evident and the simulation debug time is also greatly reduced.
Assertion-based verification is a multi-faceted approach to verifying a collection of partial specifications more efficiently. SystemVerilog Assertions enable capabilities for both simulation and formal verification and directly address the limitations of today’s verification flows.
Hope you have enjoyed this introduction and you can look forward to the next article which will discuss the use of implication in assertions and its importance in assertions.
To learn SystemVerilog in detail, explore our Advanced ASIC Verification Course.