SystemVerilog Assertions: Same Cycle and Next Cycle Implication

🔗 Same Cycle and Next Cycle Implication

#

In SystemVerilog assertions, implication operators are used to define temporal expressions from a condition to a result:

✅ Same Cycle Implication (|->)

#

• The right-hand side must be true in the same cycle or at the same clock edge as the left-hand side.
• Simply put, “Condition and result must happen on the same clock edge.”

Example:

assert property (@(posedge clk) (a && b) |-> (x && y));

In this example:

• a && b must happen concurrently with x && y on the same cycle.

✅ Next Cycle Implication (|=>)

#

• The right-hand side must be true in the cycle following the left-hand side.
• That is, the right-hand side is evaluated one cycle later.

Example:

assert property (@(posedge clk) (a && b) |=> (x && y));

In this example:

• If a && b happens in one cycle, then x && y is expected in the next cycle.

🔁 Assertion Overlapping

#

When writing assertions, temporal expressions (such as ##, |->) span multiple clock cycles. Using overlapping, multiple assertions can be active at the same time. For example:

assert property (@(posedge clk) (a ##1 b ##1 c));

Here:

• The assertion starts when a is active,
• b is checked one cycle later,
• c is checked another cycle later.
• This assertion can restart at every clock cycle and overlaps.

⚡ Useful Functions

#

SVA provides many useful functions that can be used within assertions. Here are the most common ones:

✅ $rose and $fell

#

• $rose(signal): Detects a rising edge from 0 to 1.
• $fell(signal): Detects a falling edge from 1 to 0.

Example:

assert property (@(posedge clk) $rose(req) |-> ack);

This checks ack at the rising edge of the req signal.

✅ $past

#

• $past(expression, N): Returns the value of an expression from N cycles ago (default N=1).
• Often used with reset checks.

Example:

assert property (@(posedge clk) (reset == 0) |-> (data == $past(data)));

This checks whether data has remained stable when reset is inactive.

✅ $stable()

#

• $stable(signal): Tests that a signal has not changed during the same clock cycle.
• Ideal for glitch detection.

Example:

assert property (@(posedge clk) $stable(data));

✅ $countones()

#

• $countones(vector): Returns the number of bits that are 1 in a vector.
• Useful for popcount applications.

Example:

assert property (@(posedge clk) ($countones(control_bus) <= 1));

This ensures that at most one bit is active on the bus at the same time.

✅ $isunknown()

#

• $isunknown(signal): Checks whether a signal is X or Z (unknown).

Example:

assert property (@(posedge clk) !$isunknown(data));

✅ $onehot() and $onehot0()

#

• $onehot(vector): Checks that only one bit in the vector is 1.
• $onehot0(vector): Checks that either only one bit is 1 or all bits are 0.

Example:

assert property (@(posedge clk) $onehot(state));

This is commonly used for FSM state checking.