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

OVL_ASSERT_2STATE, // defined as enum types
OVL_ASSERT: begin : ovl_assert
if (min_ack_cycle > 0)
begin : a_assert_handshake_ack_min_cycle
A_ASSERT_HANDSHAKE_ACK_MIN_CYCLE_P:
assert property (ASSERT_HANDSHAKE_ACK_MIN_CYCLE_P)
else ovl_error_t("...as before...");
end
// other assert and assume statements
endcase
'endif //ASSERT_ON

'ifdef COVER_ON
generate
if (coverage_level != OVL_COVER_NONE) begin : ovl_cover
if (OVL_COVER_BASIC_ON)
begin : ovl_cover_basic
cover_req_asserted:
cover property
(reset throughout req))
ovl_cover_t("req_asserted covered");

end
//... other cover statement ...
end
endgenerate
'endif // COVER_ON t

Notice the following differences:

￿ Case default values on parameters are removed since constant argument values
are checked at compile time.
￿ Case item labels are predefined enum types rather than 'define symbols.
￿ The property expressions use property operators to allow sequences as the
arguments and to make the assertions more efficient for formal tools. For example,
in property ASSERT_HANDSHAKE_ACK_MIN_CYCLE_P , the sequence repetition is
replaced by not s_eventually ... to accept a sequence expression for ack .
￿ Since both req and ack can be sequences, $rose had to be removed from both
of these operands of the property. Thus, if the user wishes to use $rose on a
Boolean, the appropriate expression has to be passed as the actual argument. 2

Note that by extending the type of the arguments to sequence ,itisnow
impossible to include checks for the presence of x/z values in the variables involved
in the actual arguments. If such checking is required, the best approach is to
create specific checkers just for the purpose of verifying x/z on variables. An
open question remains how to disable existing assertions within the checker in such
cases. It requires either an enhancement to the SystemVerilog language to provide

2 If a system function existed that allowed to distinguish Boolean expressions from temporal
sequences and properties, a conditional generate could be used to construct different forms of
properties depending on the actual argument.