SystemVerilog Sequence, Sequence Implication, and Usage

🔗 What is a Sequence?

#

In SVA, a sequence is a sequential specification of one or more temporal expressions. Sequences allow us to define time-based relationships.

Example:

sequence s_handshake;
  req ##1 ack;
endsequence

Here:

• After req, the ack signal is expected one cycle later.

🔀 Sequence Implication

#

When writing a property with a sequence, sequence implication is used. This means that if one sequence occurs, another sequence is expected to follow.

assert property (@(posedge clk) s_handshake |-> data_valid);

⏸️ Overlapping vs. Non-Overlapping Sequence Implication

#

✅ Overlapping Sequence Implication (|->)

#

• The right-hand side of the sequence starts in the same cycle that the left-hand side ends (overlapping).
• In other words: “The right side starts immediately after the left side ends.”

Example:

assert property (@(posedge clk) s1 |-> s2);

✅ Non-Overlapping Sequence Implication (|=>)

#

• The right-hand side of the sequence starts one cycle after the left-hand side completes.
• In other words: “Left side ends, then the right side starts in the next cycle.”

Example:

assert property (@(posedge clk) s1 |=> s2);

📝 Conditional and Unconditional Properties

#

• Unconditional Property: Starts directly with a sequence or expression.

  assert property (@(posedge clk) count < 5);
  

• Conditional Property: Similar to an if...else structure, e.g., data_valid is expected if enable is high.

  assert property (@(posedge clk) (enable |-> data_valid));
  

Here, disable iff disables the assertion in a reset state.

🚫 Never Properties

#

Sometimes we want an event to never occur. This is achieved with the not keyword.

Example:

assert property (@(posedge clk) not (error));

This property means the error signal should never be 1.

⚡ Using $rose and $fell in Sequences

#

The $rose() and $fell() functions can be used in sequences to detect signal transitions.

Example:

sequence s_rising_edge;
  $rose(signal);
endsequence

This sequence captures the transition of signal from 0 to 1.

🚦 Disabling Properties

#

The disable iff construct is used to disable an assertion under certain conditions.

Example:

assert property (@(posedge clk) disable iff (reset) (req |-> ack));

Here, the assertion is disabled when reset is active.

⚙️ Default Disable Statement

#

Instead of writing disable iff for each property individually, you can define a global disable:

default disable iff (reset);

In this case:

• All properties are disabled when reset is active.
• Improves code readability.