assert_implication
Ensures that a specified consequent expression is TRUE if the specified antecedent expression is TRUE.
|
Parameters:
severity_level
property_type
msg
coverage_level
|
Class:
single-cycle assertion
|
Syntax
assert_implication
[#(severity_level, property_type, msg, coverage_level )]
instance_name (clk, reset_n, antecedent_expr, consequent_expr );
Parameters
|
severity_level
|
Severity of the failure. Default: ‘OVL_ERROR.
|
|
property_type
|
Property type. Default: ‘OVL_ASSERT.
|
|
msg
|
Error message printed when assertion fails. Default: “VIOLATION”.
|
|
coverage_level
|
Coverage level. Default: ‘OVL_COVER_ALL.
|
Ports
|
clk
|
|
Clock event for the assertion. The checker samples on the rising edge of the clock.
|
|
reset_n
|
|
Active low synchronous reset signal indicating completed initialization.
|
|
antecedent_expr
|
Antecedent expression that is tested at the clock event.
|
|
consequent_expr
|
Consequent expression that should evaluate to TRUE if antecedent_expr evaluates to TRUE when tested.
|
Description
The assert_implication
assertion checker checks the single-bit expression antecedent_expr at each rising edge of clk. If antecedent_expr is TRUE, then the checker verifies that the value of consequent_expr is also TRUE. If antecedent_expr is not TRUE, then the assertion is valid regardless of the value of consequent_expr.
Assertion Check
|
ASSERT_IMPLICATION
|
Expression evaluated to FALSE.
|
Cover Point
|
cover_antecedent
|
The antecedent_expr evaluated to TRUE.
|
Notes
1. This assertion checker is equivalent to:
assert_always
[#(severity_level, property_type, msg, coverage_level )]
instance_name (clk, reset_n, (antecedent_expr ? consequent_expr : 1’b1 ));
See also
assert_always, assert_always_on_edge, assert_never, assert_proposition
Example
assert_implication #(
|
|
‘OVL_ERROR,
‘OVL_ASSERT,
“Error: q valid but q full”,
‘OVL_COVER_ALL)
|
// severity_level
// property_type
// msg
// coverage_level
|
|
not_full (
|
|
|
|
clk,
reset_n,
q_valid,
q_not_full );
|
// clock
// reset
// antecedent_expr
// consequent_expr
|
Ensures that q_not_full
is TRUE at each rising edge of clk
for which q_valid
is TRUE.
|
© Accellera Organization, Inc. 2005 All Rights Reserved.
|
Standard OVL V1.1a
|