Immediate and Concurrent Assertions

SystemVerilog has two kinds of assertions. An immediate assertion checks a condition at one moment, like an if statement that complains. A concurrent assertion checks a rule at every clock edge and can describe behavior over several cycles. This article explains both, shows when each one is checked, and maps them to the form that ChipVerify Lab reads.

9 min read | Beginner to Intermediate

What You'll Learn

• Write immediate and concurrent assertions and explain when each one is checked
• Use labels, action blocks and disable iff
• Explain sampled values and why a concurrent assertion ignores glitches
• Translate both kinds into the form the lab engine reads

Immediate Assertions

An immediate assertion is a statement inside procedural code, such as an always block, a task or a function. It checks its condition at the moment the code runs, just like an if:

always_comb begin
  a_sat_imm: assert (y >= a && y >= b)
    else $error("sum %0d + %0d gave %0d", a, b, y);
end

The parts:

• a_sat_imm: is a label. It names the assertion in logs and reports. Always label your assertions.
• assert (expression) is the check.
• else $error(...) is the action block, run when the check fails. Without it a simulator reports an error by default. $fatal, $warning and $info set other severities.

Immediate assertions are good for combinational rules and for checks inside testbench code. Their weakness in simulation is that combinational code can run several times in one time step while the signals settle. A plain immediate assertion may then fail on a value that is only there for a moment. A deferred immediate assertion, written assert final (...) or assert #0 (...), waits until the values have settled before it reports.

Concurrent Assertions

A concurrent assertion describes a rule that is checked at every clock edge:

a_sat: assert property (@(posedge clk) y >= a && y >= b)
  else $error("saturating add failed");

• assert property marks it as concurrent.
• @(posedge clk) is the clocking event: the rule is evaluated at each rising edge.
• The body can be a simple expression, as here, or a sequence over several cycles, as the sequences and implication article shows.

Concurrent assertions are usually written at module level, next to the logic they describe. They can also be placed inside an always or initial block, but module level is the common style.

Sampled Values

A concurrent assertion does not use the values that signals have after the clock edge. It uses the values sampled just before the edge, the same values that the flip-flops capture. So the assertion sees exactly what the registers see, and a short glitch between two edges is invisible to it.

In formal verification this difference is mostly about which checks you want: a combinational rule that must hold all the time, or a rule about the clocked behavior. A formal tool treats both precisely.

disable iff

Most rules make no sense during reset. disable iff (rst) turns the check off while rst is high:

a_max: assert property (@(posedge clk) disable iff (rst) q <= 4'd12);

If rst goes high in the middle of a multi-cycle check, that check is abandoned and counts as neither pass nor fail. A design usually has many assertions with the same clock and reset, so SVA lets you set defaults once per module:

default clocking cb @(posedge clk); endclocking
default disable iff (rst);

a_max: assert property (q <= 4'd12);   // uses the defaults

An Example: a Saturating Adder

A saturating adder adds two 8-bit numbers and gives 255 when the sum does not fit, instead of wrapping around. Audio and image processing use this, because a wrapped value would turn a loud sample into a quiet one. This version has a bug in the overflow test:

module sat_add (input clk, input [7:0] a, input [7:0] b,
                output [7:0] y, output reg [7:0] q);
  assign y = (a[7] & b[7]) ? 8'd255 : a + b;   // bug: misses overflows like 200 + 100
  always @(posedge clk) q <= y;
endmodule

The designer assumed that a sum overflows only when both numbers are 128 or more. But 200 + 100 also overflows, and only one of them is that large. A rule that catches it without spelling out the overflow logic: the result of a saturating add is never smaller than either input.

a_sat_imm: assert (y >= a && y >= b);                           // in an always_comb block
a_sat:     assert property (@(posedge clk) y >= a && y >= b);    // at module level

Running It in ChipVerify Lab

The lab front end reads immediate assert statements, but not assert property, labels with action blocks, or disable iff. The two forms translate like this:

For the adder:

`ifdef FORMAL
  // immediate assertion on the combinational output
  always @(*) assert (y >= a && y >= b);
  // the same rule, checked only at the clock edge (the lab form of a concurrent assertion)
  always @(posedge clk) assert (y >= a && y >= b);
`endif

The run fails at once. The combinational check fails in step 0, the very first state, because it needs no history. The counterexample is a single set of input values: a = 223, b = 95, and y = 62. The true sum is 318, which does not fit in 8 bits, so the result should be 255. With only the clocked check, the same values are found and reported in step 1, the usual one-step delay of a clocked assertion in the lab engine.

The fix compares the full 9-bit sum with 255:

assign y = ({1'b0, a} + {1'b0, b} > 9'd255) ? 8'd255 : a + b;

With it, both checks pass.

Common Mistakes

wire [8:0] sum9 = {1'b0, a} + {1'b0, b};
always @(*) assert (y == (sum9 > 9'd255 ? 8'd255 : sum9[7:0]));