Checker Libraries - SVA: The Power of Assertions in SystemVerilog - page 548

default disable iff rst_n;
onehot0 A1(r1); // check input
always_comb begin
r2=r1;
onehot0 A2(r1); // check output
end
endmodule

t

As with the previous simple combinational checker (Sect. 24.3.1 ), this more
complex checker can still be instantiated both inside (instance a1 ) and outside
(instance a2 ) a procedure. Both checker instances use default values for configura-
tion constants and enable verification statement assert final because ASSERT_ON
is defined and usage_kind default value of ASSERT is used. Coverage is globally
disabled because COVER_ON is not defined.

24.3.3 A Simple Property-Based Temporal Checker

We now turn our attention to checkers that verify behavior over time-temporal
checkers.
Similarly as with the simple combinational checker and let declarations, we can
define a simple temporal, clocked, checker using property declarations. As before,
we assume that default disable iff defines an active low reset.
Example 24.6. property -based temporal checker
property time_interval_p
( sequence trig, property cond,
start_tick = 1, end_tick = 1,
event clk = $inferred_clock,
untyped rst_n = $inferred_disable);
@clk disable iff (! bit '(|rst_n))
trig |->
always [start_tick:end_tick] cond;
endproperty : time_interval_p

t

Note that in the consequent of |-> we used the always operator instead of using
the consecutive repetition cond[ * start_tick:end_tick] . The reason is that we
obtain maximum generality as to the actual argument for the formal cond . It can not
only be a Boolean or a sequence , but also any property expression.
The property verifies that when trig occurs cond holds true in the interval
start_tick to end_tick clock ticks, unless it is disabled by rst_n being 1'b0 .
The property has the following characteristics:

￿ The actual argument for trig is restricted to the type sequence because it is used
in the antecedent of |-> . The actual argument for cond can be any property
expression (Boolean, sequence or property). The actual argument for clk must be
a clocking event, while rst_n is left untyped for the user to be able to pass any
valid expression.