Formal Verification and Models - SVA: The Power of Assertions in SystemVerilog - page 473

21.7 Immediate and Deferred Assertions

So far in this chapter we have dealt only with concurrent assertions. Immediate
and deferred assertions (both observed and final) are also meaningful for FV when
they are instantiated in synthesizable code and when the data they reference are
synthesizable. For FV, there is no difference between immediate and deferred
assertions (observed and final). Therefore, we limit our discussion to deferred
assertions.
For FV, a possible implementation of deferred assertions is to transform them into
(possibly embedded) concurrent assertions using the following scheme: assertion
assert final (e); is transformed into assertion assert property (@clk e);
for some clock clk . Assumptions and cover statements are transformed similarly.
It remains to define the clock for the transformed assertions.
If the deferred assertion is not in the scope of an always procedure such that
the clock is inferable from it for concurrent assertions, the global clock is inferred.
The global clock is inferred even if there is no global clocking definition in the
design: recall that global clocking is only required to map the global clock into
an event for simulation, and in FV models the global clock is inherently defined .

Example 21.33. Consider the following code fragment:

a1: assert #0 (e1);

always_comb begin
// ...
if (en) begin
// ...
a2: assert #0 (e2);
end else // ...
end
For FV, this code is rewritten using concurrent assertions as follows:

a1: assert property (@$global_clock e1);

always_comb begin
// ...
if (en) begin
// ...
a2: assert property (@$global_clock e2);
end else // ...
end

t

If the deferred assertion is in the scope of an always procedure with an inferable
clock then this deferred assertion is treated in FV as a concurrent assertion.