assert_no_transition
Ensures that the value of a specified expression does not transition from a start state to the specified next state.
|
Parameters:
severity_level
width
property_type
msg
coverage_level
|
Class:
2-cycle assertion
|
Syntax
assert_no_transition
[#(severity_level, width, property_type, msg, coverage_level )]
instance_name (clk, reset_n, test_expr, start_state, next_state );
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 not 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 invalid 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 not equal next_state on the current rising edge of clk.
|
Description
The assert_no_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 so, 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) do not transition to invalid values.
Assertion Check
|
ASSERT_no_transition
|
Expression transitioned from start_state to a value equal to 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.
See also
assert_transition
Example
assert_no_transition #(
|
|
‘OVL_ERROR,
3,
‘OVL_ASSERT,
“Error: bad state transition”,
‘OVL_COVER_ALL)
|
// severity_level
// width
// property_type
// msg
// coverage_level
|
|
valid_transition (
|
|
|
|
clk,
reset_n,
current_state,
requests > 2 ? ‘FULL : ‘ONE_IN_Q,
‘EMPTY;
|
// clock
// reset
// test_expr
// start_state
// next_state
|
Ensures that current_state
does not transition to ‘EMPTY improperly. If requests
is greater than 2 and the current_state is ‘FULL, current_state
should not transition to ‘EMPTY in the next cycle. If requests
is not greater than 2 and current_state
is ‘ONE_IN_Q, current_state
should not transition to ‘EMPTY in the next cycle.
|
© Accellera Organization, Inc. 2005 All Rights Reserved.
|
Standard OVL V1.1a
|