assert_transition

Ensures that the value of a specified expression transitions properly from a start state to the specified next state.


	Parameters: severity_level width property_type msg coverage_level	Class: 2-cycle assertion

Syntax

Parameters


	severity_level	Severity of the failure. Default: ‘OVL_ERROR.
	width	Width of the test_expr argument. Default: 1.
	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.
test_expr	[ width - 1: 0 ]	Expression that should transition to next_state on the rising edge of clk if its value at the previous rising edge of clk is the same as the current value of start_state.
start_state	[ width - 1: 0 ]	Expression that indicates the start state for the assertion check. If the start state matches the value of test_expr on the previous rising edge of clk, the check is performed.
next_state	[ width - 1: 0 ]	Expression that indicates the only valid next state for the assertion check. If the value of test_expr was start_state at the previous rising edge of clk, then the value of test_expr should equal next_state on the current rising edge of clk.

Description

The assert_transition assertion checker checks the expression test_expr and start_state at each rising edge of clk to see if they are the same. If so, the checker evaluates and stores the current value of next_state. At the next rising edge of clk, the checker re-evaluates test_expr to see if its value equals the stored value of next_state. If not, the assertion fails. The checker returns to checking start_state in the current cycle (unless a fatal failure occurred)

The start_state and next_state expressions are verification events that can change. In particular, the same assertion checker can be coded to verify multiple types of transitions of test_expr.

The checker is useful for ensuring certain control structure values (such as counters and finite-state machine values) transition properly.

Assertion Check


	ASSERT_TRANSITION	Expression transitioned from start_state to a value different from next_state.

Cover Point


	start_state	Expression assumed a start state value.

Notes

1. The assertion check compares the current value of test_expr with its previous value. Therefore, checking does not start until the second rising clock edge of clk after reset_n deasserts.

assert_transition #(
	‘OVL_ERROR, 3, ‘OVL_ASSERT, “Error: bad count transition”, ‘OVL_COVER_ALL)		// severity_level // width // property_type // msg // coverage_level
	valid_count (
		clk, reset_n, count, 3’d3, (sel_8 == 1’b0) ? 3’d0 : 3’d4 );	// clock // reset // test_expr // start_state // next_state