Checkers - SVA: The Power of Assertions in SystemVerilog - page 209

a two-state integral, such as bit , and 'X if its actual type is a four-state integral, such
as logic . If we want it always be initialize it with '0 , we should do it explicitly:
checker out_inferred (in,
output var type (in) out = '0,
input event clk);

always_ff @clk
out <= in;

t

9.5.1.3 Semantics of Checker Output Arguments

Actual checker output arguments, of course, must be L-values.

Example 9.28. The instance good of checker out_inferred defined in

Example 9.26 is legal, whereas the instance bad is not:
logic x, y, clock;
...
out_inferred good(x, y, posedge clock);
out_inferred bad(x, !y, posedge clock);
This is because y is an L-value, and !y is not. t

Checker output argument simulation semantics is similar to that of programs
(see Sect. 3.5 ). The checker instantiation is treated as if there were continuous
assignments of the checker output formal arguments to their corresponding actual
arguments. These implicit continuous assignments are executed in the Reactive
region.

Example 9.29. Consider the following instantiations of checker out_inferred
defined in Example 9.26 :

wire dest;
logic src1, src2, clock;
...
out_inferred inst1(src1, dest, posedge clock);
out_inferred inst2(src2, dest, posedge clock);
Here the net dest is driven by outputs of two instantiations of checker
out_inferred . These outputs are of type logic according to the type of the
checker instantiation inputs. The value conflict is resolved according to the standard
SystemVerilog resolution rules for nets.
The situation described in this example is rare, and in most cases in practice a
checker output is a single driver of the corresponding variable or net. t