Using Boolean Expressions and Assertions in SystemVerilog

🧩 Similarities Between Boolean Expressions and Assertions

#

Assertions can be thought of as simple boolean expressions. For example:

assert(a && b);

actually works like this:

if (!(a && b))
  $error("Assertion failed");

That is, assertions check the condition at runtime and alert the simulation if it fails.

📌 Assertion Directives (assert, assume, cover, restrict)

#

In SystemVerilog, assertions are defined using 4 main directives:

✅ assert – Checks whether the design behavior is correct. – If the assertion fails, it generates an error message. – Example:

assert property (req |-> ##1 ack);

✅ assume – Used for formal verification tools and indicates that the design assumes certain external conditions. – Behaves similarly to assert in simulation. – Example:

assume property (clk == 1'b1);

✅ cover – Checks whether a certain design behavior occurs. – Can be used for functional coverage during design verification. – Example:

cover property (req && ack);

✅ restrict – Used to constrain the design space. – Applied in formal verification and usually has no effect in simulation. – Example:

restrict property (reset == 0);

🚦 What is an Immediate Assertion?

#

Immediate assertions are assertions that are used inside procedural blocks (initial, always, always_ff, always_comb, etc.) and are evaluated immediately. They are used for combinational checks and to catch errors right away.

Example:

always_ff @(posedge clk) begin
  assert (data_valid) else $error("Data not valid!");
end

This construct checks data_valid on every clock edge and prints an error message if it fails.

⏳ What is a Deferred Immediate Assertion?

#

Deferred immediate assertions are also used inside procedural blocks but defer their check to the next delta cycle. This means the check is not done immediately but after the block finishes. This is useful for ensuring data consistency, especially with non-blocking assignments.

Example:

always_ff @(posedge clk) begin
  x <= y; // non-blocking assignment
  assert final(x == y); // deferred immediate assertion
end

Here, the final keyword marks it as a deferred immediate assertion, and the assertion is evaluated after the block completes (at the delta cycle).

Immediate vs. Deferred Immediate

#

🔍 Summary

#

In this section, we learned:

• That assertions are similar to simple boolean expressions,
• The differences between assert, assume, cover, and restrict,
• The concepts of immediate and deferred immediate assertions.