Assertions

Assertions are formal statements embedded in a design or testbench that specify the expected behavior of signals over time. In traditional simulation, an engineer manually checks output values after applying stimuli. Assertions automate this checking by continuously monitoring the design and flagging violations as soon as they occur. SystemVerilog Assertions (SVA) provide a rich, standardized language for expressing temporal properties that would be impractical to check manually in complex designs.

Core Concept Explanation

SVA has two fundamental categories of assertions. The first is immediate assertion, which is an assertion statement placed inside a procedural block (initial or always). It behaves like a conditional check and evaluates the expression at the exact simulation time it is executed. If the expression is false, the simulator reports an assertion failure with the location and time. Immediate assertions do not involve time windows or clock edges.

The second category is concurrent assertion, which is clock-based and checks properties that span multiple clock cycles. These are written outside procedural blocks, directly in the module body or inside interface blocks. Concurrent assertions are continuously evaluated on every specified clock edge throughout the simulation. They are the primary mechanism for expressing temporal relationships such as handshake protocols, bus arbitration rules, and pipeline timing constraints.

SVA Building Blocks: Sequence and Property

A sequence in SVA describes a series of signal behaviors across clock cycles. Sequences use the ##N delay operator to say N clock cycles later. For example, a ##2 b means: a is true now, and b is true 2 cycles later. A property wraps a sequence with a logical implication or other temporal operator to create a checkable rule. The implication operator |-> is the overlapping implication: if the antecedent holds at cycle N, the consequent is checked starting at cycle N.

The non-overlapping implication |=> is equivalent to |-> ##1. It means if the antecedent holds at cycle N, the consequent is checked starting at cycle N+1. This is the more intuitive form for request-acknowledge protocols where the acknowledge is expected the cycle after the request. The three SVA directives are assert property (checks and reports failure), assume property (constrains input assumptions in formal verification), and cover property (tracks whether a sequence was ever exercised during simulation).

Mathematical Expression

The overlapping implication in SVA follows the logical form: for every clock cycle N where the antecedent A(N) is true, the consequent B(N+k) must be true where k is the cycle offset. Formally: A(N) = true IMPLIES B(N+k) = true, for all N. If A(N) is false at any cycle, the property vacuously passes for that cycle without evaluating B. Vacuous passing is a significant concern in formal verification and is tracked separately. The delay operator ##k increments the cycle reference by k. Multiple delays can be chained: A ##1 B ##2 C means A true at cycle 0, B true at cycle 1, C true at cycle 3.

Practical Understanding

In industry, assertions are written for every significant interface protocol in a design. A typical AXI bus interface will have dozens of assertions covering valid-ready handshake rules, burst length constraints, and address alignment requirements. These assertions catch protocol violations the instant they occur rather than requiring engineers to manually trace simulation waveforms. When assertions are synthesized into the design for silicon-level debug (using embedded logic analyzers), the technique is called assertion-based debug.

Assertions also serve as executable documentation. Instead of reading a protocol specification document and hoping the RTL implements it correctly, the SVA assertions directly encode the specification as checkable properties. This makes assertion review a form of design review. For GATE aspirants, it is important to understand the difference between assert (checking), assume (constraining), and cover (measuring reachability), as these often appear in multiple-choice questions.

Given:
A synchronous FIFO interface has two signals: wr_en (write enable) and full (FIFO full flag).
Protocol rule: if wr_en is asserted when full is high, it is a violation.
Clock: posedge clk.

Why this formula applies:
Concurrent assertion with overlapping implication |-> checks:
If (wr_en AND full) at any rising clock edge, the consequent must be false.
Since the violation IS the condition itself, assert that the condition never occurs.

Formula:
  property no_write_when_full;
    @(posedge clk) (wr_en && full) |-> 0;
  endproperty
  assert property (no_write_when_full)
    else $error("FIFO write violation at time %0t", $time);

Substitution:
At time 50ns: wr_en = 1, full = 1 -> antecedent is TRUE
Consequent is 0 (always false) -> assertion FAILS
Simulator prints: "FIFO write violation at time 50"

Alternative cover form:
  cover property (@(posedge clk) wr_en && !full);
  (checks if a valid write ever occurred during simulation)

Final Answer:
Assertion catches FIFO overflow attempt at 50ns.
cover property tracks that at least one valid write was exercised.

Exam Tip: |-> is overlapping implication (check starts same cycle as trigger). |=> is non-overlapping (check starts one cycle after trigger). ##N means exactly N cycles later. Questions mixing these operators are common in advanced Verilog MCQs.

Mechanism: Concurrent Assertion Evaluation Flow

• Immediate assertions check a Boolean expression at the exact simulation time they execute, with no concept of clock cycles or time windows.
• Concurrent assertions are evaluated on every specified clock edge. They can check sequences that span multiple clock cycles using ##N delay operators.
• |-> overlapping implication: consequent checked starting at the same clock cycle as the antecedent. |=> non-overlapping: consequent checked one cycle later.
• assert property: simulation reports failure if property is violated. assume property: formal tool treats this as an input constraint, not a check.
• cover property: checks if a sequence was ever reached during simulation. It passes when the sequence occurs at least once, and is used for coverage tracking.

Quick Revision

• Two types: immediate assertion (procedural, instant check) and concurrent assertion (clock-based, temporal check).
• Sequence ##N: N clock cycles later. A ##1 B means B must be true exactly 1 cycle after A.
• |-> overlapping implication: same cycle check. |=> non-overlapping: next cycle check. |=> is shorthand for |-> ##1.
• Three SVA directives: assert (check), assume (constrain for formal), cover (reachability tracking for coverage).
• SVA syntax: property name; @(posedge clk) antecedent |-> consequent; endproperty; assert property (name);
• Vacuous pass: if antecedent is never true, property trivially passes. Use cover property to detect this situation.
• Exam trap: |-> checks consequent at SAME cycle as trigger. |=> checks consequent one cycle LATER. Mixing these two is a common exam error.