Logic Design - Assertions in SystemVerilog

Logic Design - Assertions in SystemVerilog | Ecency

[Edit of Image1]

Introduction

Hey it's a me again @drifter1!

Today we continue with the Logic Design series on SystemVerilog in order to talk about Assertions.

So, without further ado, let's get straight into it!

Assertions

Assertions are used for the purpose of verification. They specify the expected behavior of a design and are commonly used in Functional Coverage. More specifically, properties of the design are checked by an assertion and if the behavior is unexpected the assertion will fail.

It's possible to write assertions in the usual procedural fashion (always blocks and conditional statements), but this makes the code difficult to maintain and scale, as shown below.

always @ (posedge clk)
begin
    if (!expression)
        // assertion failed
end

Thus, SystemVerilog provides assertions in the form of a declarative language.

For example:

assert property (@ (posedge clk) expression);

Types

SystemVerilog provides two types of assertions:

Immediate Assertions : which follow simulation event semantics and are executed like statements in procedural blocks.
Concurrent Assertions : which are based on clock semantics and get evaluated every time, like an always block with a clock.

Immediate Assertions

Immediate Assertions are included in procedural blocks and can be as simple as:

assert (expression);

which operates just like an if statement.

They can optionally include a label (but one is assigned by the simulator either way) and different code for pass / fail of the conditions (like an if-else).

assert_label : assert (expression) begin
    // if condition is true (pass)
end else begin
    // if condition is false (fail)
end

For example, such an assertion can be placed on the randomization method (randomize) for constraints, because it returns 1 if the randomization is successful, as shown below.

initial begin
    className instance = new();

    assert (instance.randomize());
end

Concurrent Assertions

A concurrent assertion can be distinguished from an immediate assertion easily as it is always tied to a clock definition and uses the keyword property.

It has the following layers:

boolean
sequence
property
assert property

Boolean Expressions

The Boolean layer is where the conditions are specified. All operators except the assignment, increment and decrement operators can be used in it. It's also possible to include function calls, but with no output or ref arguments.

Sequence

The conditions are included in a sequence and are checked at every clock event. Sequential checks that may take several clock cycles can be achieved using the ## operator, which is followed by some time delay.

A sequence has the following syntax:

sequence seq_id;
    // boolean expressions / conditions
endsequence

Property

Sequences can be combined into properties. Either the sequence or the property must include some kind of clocking event, so that assertion is possible.

A property has the following syntax:

property prop_id;
    // boolean expressions / conditions
    // or
    // sequence identifiers
endproperty

Assert

The actual assertion comes in the form of the assert declaration, which has the following syntax:

assert property (conditions or seq_id or prop_id);

So, the parentheses can reference a sequence or property defined earlier, or specify the conditions (including the clock event) directly.

Assume, Cover and Expect

SystemVerilog also includes the assume, cover and expect verification statements, which have the same exact syntax as the assert statement.

The assume statement specifies a property as assumption and is used with formal verification tools.

The cover statement monitors a given property and reports the coverage.

The expect statement can be used inside a procedural block for the purpose of waiting until a property evaluates to true or false.

RESOURCES:

References

Images

https://www.flickr.com/photos/creative_stock/5227842611

Block diagrams and other visualizations were made using draw.io

Previous articles of the series

Verilog

Introduction → Basic Syntax, Data Types, Operators, Modules
Combinational Logic → Assign Statement, Always Block, Control Blocks, Gate-Level Modeling and Primitives, User-Defined Primitives
Combinational Logic Examples → One Circuit - Four Implementations, Encoder, Decoder, Multiplexer
Sequential Logic → Procedural Blocks (Initial, Always), Blocking and Non-Blocking Assignments, Statement Groups
Sequential Logic Examples → Flip Flops (DFF, TFF, JKFF, SRFF), N-bit Counter, Single-Port RAM
Finite-State Machines → Finite-State Machine (FSM), FSM Types, State Encoding, Modeling FSMs in Verilog
Finite-State Machine Examples → Moore FSM Example (1 and 2 always blocks), Mealy FSM Example (1, 2 and 3 always blocks)
Testbenches and Simulation → Testbenches (DUT / UUT, Syntax, Test Cases), System Tasks, Simulation Tools
Combinational Logic Testbench Example → Half Adder Implementation, Testbench and Simulation
Sequential Logic Testbench Example → Sequence Detector FSM Implementation, Testbench and Simulation
Functions and Tasks → Function and Task Syntax, Calling, Rules, Examples
Module Parameters and Generate Block → Parameterized Module (Parameters, Instantiation and Overriding Parameters), Generate Blocks (For, If, Case)
Compiler Directives → Summary of Verilog's Compiler Directives (Include, Macros, Timescale, Conditional Compilation, etc.)
Switch Level Modeling → Transistors, Switch Primitives (NMOS, PMOS, CMOS, Bidirectional, Resistive), Signal Strengths

SystemVerilog

From Verilog To SystemVerilog → Data Types, Arrays, Structures, Operators and Expressions
Control Flow → Additional Procedural Blocks, Loops, Conditional Statements, Functions and Task Features
Processes → Fork - Join in Verilog and SystemVerilog, Process Control (wait fork, disable fork)
Events → Interprocess Communication, Events (Definition, Triggering, Waiting, Sequencing, Merging, as Arguments)
Semaphores and Mailboxes → Semaphores (Creation, Methods), Mailboxes (Definition, Methods)
Interfaces (part 1) → Interfaces (Definition, Port and Signal Lists, Instantiation), Modports
Interfaces (part 2) → Parameters, Tasks and Functions (Importing, Exporting), Clocking Blocks (Input and Output Skews)
Classes (part 1) → Classes (Definition, Constructor Function, Creating Objects, Accessing Class Members, Static and Constant Class Members, Arrays)
Classes (part 2) → Copying Objects (Shallow and Deep Copy), Inheritance, Polymorphism, Virtual Methods
Classes (part 3) → Parameterized Classes, Out-of-Block Method Declaration, Data Accessibility, Abstract / Virtual Classes
Program Blocks → Design and Testbench, Program Block (Reactive Region, Allowed Constructs)
Packages → Design Hierarchy, Packages (Definition, Importing, Definition Collision)
Constraints and Randomization → Testing and Verification, Random Variables (Standard, Random-Cyclic), Randomize Method (Constraint and Random Mode, Pre / Post Randomize)
Constraint Blocks → Constraint Blocks (Syntax, Rules), External (Explicit, Implicit), Static, Soft and In-Line Constraints
Constraint Types (part 1) → Simple Expressions, Set Membership (Inside Operator, Range, Set, Inverted), Weighted Distributions (Dist Operator, := and :/)
Constraint Types (part 2) → Conditional Relations (Implication Operator, If-Else), Iterative Constraints, Solve - Before, Random Case
Functional Coverage → Functional Coverage (Limitations, Types), Covergroups (Sampling, Coverage Points, Coverpoint Bins, Conditional Coverage, Cross Coverage, Coverage Options)