Assertion Statements - SVA: The Power of Assertions in SystemVerilog - page 67

In both cases the sensitivity list is inferred, but the inference is different leading to
potentially different behavior of the assertions:

￿ always_comb executes at time 0, while always @ * will execute only when
triggered by a value change of a signal in the sensitivity list. Consequently, an
assertion may fire at time 0 in the former case, but not in the latter.
￿ always_comb is sensitive to changes of static variables read inside a function,
while always @ * is not. Therefore, an immediate assertion inside a function may
not fire in the latter case unless the variables read in the assertion are among the
arguments of the function.
￿ Variables that are both read and written in an always_comb procedure do not
appear on the implicit sensitivity list while in always @ * they do. Therefore, an
assertion that refers to such variables in an always_comb procedure may not fire.

In RTL design code use always_comb to model combinational logic and if
needed provide checking using deferred assertions.

4.3.4 Effect of Short-Circuiting in Deferred Assertions

Short circuiting effects on deferred assertions can be even more non-intuitive than
on simple immediate assertions. The following code is similar to that in Sect. 4.2.3
except that an observed deferred assertion is used:

function bit check3bits ( bit [2:0] expr, value);
a2: assert #0 (expr > value) else
$error("a2 failure: expr = %b, value = %b", expr, value);
return (expr > value);
endfunction : check3bits
assign combined = v && check3bits(x, 3'b1);
Suppose that at some simulation time v became 1 and x became 2 . The conti-
nuous assignment is evaluated, the assertion passes and is enqueued in the deferred
assertion result queue. Later in the time step, v and x change to 0 . The continuous
assignment is re-evaluated and the result of the previous execution is flushed.
Since v is 0 , the simulator determines that combined is also 0 and by the rule
of short-circuiting it does not need to evaluate the function call. Therefore, the
assertion is not evaluated either and neither success nor failure is reported in
the Reactive region. If the order of operands in the assignment were exchanged, as
in assign combined = check3bits(x, 3'b1)&& v; the error would be detected
because the first operand is always evaluated. Alternately, && can be replaced on
scalar bits by & (a bitwise “and”) in which case short-circuiting does not apply.