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 ));

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.

Standard OVL V1.1a