SystemVerilog Assertions
Assertions are used to check design rules or specifications and generate warnings or errors in case of assertion failures. An assertion also provides function coverage that makes sure a certain design specification is covered in the verification. The methodology that uses assertions is commonly known as “Assertion Based Verification” (ABV). Assertions can be written in the design as well as the verification environment.
Advantages of using Assertions
- Checks design specifications and reports errors or warnings in case of failure.
- It improves debugging time. For example, a bug due to an illegal state transition can propagate to the output. Writing an assertion helps out to improve debugging time.
- Can be used in formal verification.
- Can be re-used across verification testbench or design.
- Can be parameterized
- Can be turned on/off based on the requirement.
Types of Assertions
- Immediate assertions
- Concurrent assertions
Immediate Assertions
An assertion that checks a condition at the current simulation time is called immediate assertions. They are executed like procedural statements like the if-else statements.
Syntax:
<label>: assert (expression) <pass_statement> else <fail_statement>
- If an expression evaluates true then pass_statement is executed, else the fail_statement is executed and said to be assertion failure. An expression evaluates to be 0, X, Z then an assertion is said to be failed.
- Both pass_statement and fail_statement in the above syntax are optional.
Assertion severity levels
- $info: indicates that the assertion failure carries no specific severity.
- $warning: run-time warning, which can be suppressed in a tool-specific manner.
- $fatal: run-time fatal
- $error: run-time error
-
Immediate Assertions Example
module design_ex (input clk, reqA, reqB, in);
always @(posedge clk) begin
assert (reqA || reqB) else $error("assertion failed");
assert (in == 0) else $warning("assertion warning for in == 0");
end
endmodule
Output:
xmsim: *E,ASRTST (./design.sv,4): (time 2 NS) Assertion tb_top.DUT.__assert_1 has failed
assertion failed
xmsim: *W,ASRTST (./design.sv,5): (time 6 NS) Assertion tb_top.DUT.__assert_2 has failed
assertion warning for in == 0
xmsim: *E,ASRTST (./design.sv,4): (time 10 NS) Assertion tb_top.DUT.__assert_1 has failed
assertion failed
xmsim: *E,ASRTST (./design.sv,4): (time 14 NS) Assertion tb_top.DUT.__assert_1 has failed
assertion failed
xmsim: *E,ASRTST (./design.sv,4): (time 26 NS) Assertion tb_top.DUT.__assert_1 has failed
assertion failed
Concurrent Assertion
An assertion that checks the sequence of events spread over multiple clock cycles is called a concurrent assertion. They execute in parallel with other always blocks concurrently, hence it is known as a concurrent assertion.
- Unlike immediate assertion, the concurrent assertion is evaluated only at clock tick. Thus, it is a clock-based evaluation model and an expression used in the concurrent assertion is always tied to a clock definition.
- The variables used in the assertions are sampled in the preponed region of the simulation time slot but it is evaluated at the observe region and execute pass/fail statements in the reactive region.
- A concurrent assertion can be declared in an always or initial block and that can be placed in an interface, program, or module block.
- An assert keyword is used to check the property.
Syntax:
<label>: assert property (<property_name(signals)>) <pass_statement> else <fail_statement>;
Property in assertion
The property keyword is to capture design specifications that span over time. It also contains a sequence of events. It distinguishes a concurrent assertion from an immediate assertion.
Syntax:
property <property_name>;
<expression or sequence>
endproperty
Property declaration
- A property can be declared in a module, clocking block, package or interface, etc.
- A property can have formal arguments.
Property usage
- The property captures design specifications and checks for design behavior.
- It can be used as an assumption in the verification environment.
- It is also used for coverage to measure that property is covered.
If assertion has simple property, then usually it is written as a part of the assert statement.
Example:
assert property (@(posedge clk) (req1 || req2));
If it is a complex property then it can be defined separately and used as the assert statement.
assert property (prop_req);
property prop_req;
@(posedge clk) disable iff (!reset_n)
req1 |=> req2 ##2 req3;
endproperty
SystemVerilog Assertions