Choosing the Right Assertions

1. Concurrent Assertions: The Synchronous Workhorse

Concurrent assertions are the backbone of SVA. They are designed to verify temporal properties that span multiple clock cycles in synchronous designs. You've been using them implicitly in our previous lessons.

Key Characteristics:

• Clock-based: They are always associated with a clocking event (e.g., @(posedge clk)).
• Declarative: They exist outside of procedural blocks like always or initial.
• Temporal: Their primary purpose is to check behavior over time using operators like ##, |->, and [*].

A typical concurrent assertion looks like this:

// Checks that if req is high, ack must follow within 1 to 3 cycles.
a_req_ack: assert property (@(posedge clk) req |=> ##[1:3] ack);

The most critical concept to grasp for concurrent assertions is when they sample their input values. They do so in the Preponed region of the SystemVerilog simulation time-slot. This means values are captured before any design logic (in always blocks) or non-blocking assignments have a chance to execute in that same time-slot. This design guarantees race-free, deterministic evaluation for synchronous logic—a major advantage.

2. Immediate Assertions: Procedural and Instantaneous

Immediate assertions are procedural statements. They behave like an if statement that triggers an error if the condition is false.

Key Characteristics:

• Procedural: They must be placed inside an always block, initial block, task, or function.
• Unclocked (by nature): They are evaluated whenever the procedural block they are in is executed.
• Instantaneous: They check a condition at a single moment in time without inherent temporal semantics.

A simple immediate assertion looks like this:

always @(posedge clk) begin
  // At every clock edge, check that read and write are mutually exclusive.
  if (state == ACTIVE) begin
    assert (read_en != write_en) else $error("Read and Write are both enabled!");
  end
end

Immediate assertions execute in the Active region by default. This is where most procedural code and continuous assignments are evaluated. This timing has profound implications, leading to both powerful use cases and dangerous pitfalls.

3. The Strategic Choice: Intent and Simulation Semantics

Your choice between concurrent and immediate assertions depends on two factors: what you are trying to verify (design intent) and how the simulator will evaluate it (semantics).

The Pitfall: Glitchy Immediate Assertions

A common interview question involves combinational logic. An engineer might write:

// Anti-pattern: DO NOT DO THIS
always @*
  a_combo_check: assert ( (a & b) == y ); // Is this a reliable check for an AND gate?

This is unreliable. Since multiple always @* blocks can execute in any order within the Active region, the assertion might evaluate before y has settled to its final value for that time step, causing a false failure. This non-determinism makes simple immediate assertions "glitchy" for checking combinational logic.

The Solution: Deferred Immediate Assertions

SystemVerilog (since the 2009 standard) provides an elegant solution: the deferred immediate assertion. By adding #0, you tell the simulator to evaluate the assertion in the Observed region, which occurs after the Active (where logic computes) and NBA (where flops update) regions.

// Correct way to check combinational logic
always_comb // Use always_comb for combinational logic
  a_combo_check: assert #0 ( (a & b) == y );

This ensures the check happens only after all values have stabilized for that time step, eliminating the race condition.

The Killer App: Checking Asynchronous Resets

Now, let's tackle a classic problem: verifying an asynchronous reset. Consider this property:
assert property (@(posedge async_reset) q == 0);

This will fail, even if the logic is correct. Why?

1. The concurrent assertion samples its inputs (q) in the Preponed region.
2. The posedge async_reset occurs.
3. The design logic reacts in the Active region and schedules q <= 0; for the NBA region.
4. The assertion evaluates using the old value of q sampled in step 1, sees it's not zero, and fails.

The correct tool here is a deferred immediate assertion, which waits until after the NBA update.

As you read, the key insight is that for asynchronous events, you must delay the check until after the design has updated. The deferred immediate assertion (assert #0) is the cleanest way to achieve this.

The correct way to check our asynchronous reset is:

always @(posedge async_reset)
  a_async_reset_check: assert #0 (q == 0) else $error("q is not 0 after async reset!");

A Decision Framework for Interviews

When an interviewer asks "Which assertion type would you use for X?", use this mental model:

1. Is the property checking a synchronous, temporal relationship over multiple clock cycles?

   • Yes: This is the 95% case. Use a concurrent assertion. It's race-free for synchronous logic and highly expressive.

2. Is the property checking an immediate reaction to an asynchronous signal (like a reset)?

   • Yes: Use a deferred immediate assertion (assert #0) inside an always block sensitive to that async signal. This correctly schedules the check after the design updates.

3. Is the property checking combinational logic that must be true at all times?

   • Yes: Use a deferred immediate assertion (assert #0) inside an always_comb block. This avoids the glitchy behavior of simple immediate assertions.

4. Is the property a sanity check at a specific point within a procedural testbench task (e.g., in a driver or monitor)?

   • Yes: A simple immediate assertion (assert) is fine here. You control the procedural flow, so there's no race condition to worry about.

Conclusion

You now have a robust framework for selecting between concurrent and immediate assertions. You've moved beyond syntax to understand the crucial role of the SystemVerilog simulation scheduler. This knowledge is key to writing correct, efficient, and defensible verification code.

Key Takeaways:

• Concurrent assertions are for synchronous, temporal properties. They sample in the Preponed region, making them ideal for clocked designs.
• Immediate assertions are for procedural, instantaneous checks. They evaluate in the Active region by default, which can be unreliable for RTL checks due to race conditions.
• Deferred immediate assertions (assert #0) are the solution for robust asynchronous and combinational checks. They evaluate in the Observed region, after the design state has stabilized.
• Your choice of assertion is a strategic decision based on design intent and an understanding of the SV scheduler (Preponed -> Active -> NBA -> Observed).

In the next lesson, we will apply these concepts to write specific assertions for data integrity checks, such as verifying data stability and preventing data corruption—common tasks in any verification plan.

🧠 Interview & Practice Drill

Let's put this knowledge to the test.

🎤 Interview Drill Section

1. Rapid Fire Theory:

   • An interviewer says, "I want to check that my asynchronous reset puts my FIFO's empty flag to 1. I wrote assert property (@(posedge rst_n) fifo_empty);. Why is my team lead telling me this is wrong?"
   • What is the difference in execution timing between a simple immediate assertion and a deferred immediate assertion? Name the relevant simulation regions.
   • When would you ever use a simple assert instead of assert #0 or a concurrent assertion? Give a concrete example.
   • "Performance is critical. Is it better to write 100 individual assertions for a 100-bit bus comparison or one assertion on the whole bus?"

2. Scenario-Based Problem:

   • You are verifying a module with a configuration register CFG that is written once at time zero and should never change. You need to write a property to ensure CFG remains stable.
   • Question: What are two different ways you could verify this using SVA? Discuss the pros and cons of each approach.
     • (Hint 1: A concurrent approach using $stable()).
     • (Hint 2: An immediate approach using $past()).

🧩 Coding Exercises

Write the SVA code for the following scenarios. Assume a default clock posedge clk.

1. Asynchronous Set: A register status_reg has a synchronous clear on clk but an asynchronous set input (async_set). When async_set goes high, status_reg should immediately become 1. Write a robust assertion to check this behavior.

2. Combinational Decoder: You have a 3-to-8 decoder with a 3-bit input addr and an 8-bit one-hot output sel. Write an assertion to verify that for any given addr, the correct sel bit is high and all others are low. For example, if addr is 3'b101, then sel[5] must be 1. The check should be robust against glitches.

3. Procedural Check in a Task: You have a testbench task write_bus(input [31:0] data, input [15:0] addr);. Inside this task, before driving the signals, you need to assert that the address is within a valid range (e.g., 16'h1000 to 16'hFFFF). Write the task with the appropriate assertion.