diff --git a/osvvm_fsm_coverage/osvvm_fsm_coverage.vhd b/osvvm_fsm_coverage/osvvm_fsm_coverage.vhd index 1001423..188b871 100644 --- a/osvvm_fsm_coverage/osvvm_fsm_coverage.vhd +++ b/osvvm_fsm_coverage/osvvm_fsm_coverage.vhd @@ -112,9 +112,14 @@ begin -- psl default clock is rising_edge(s_clk); - -- psl IDLE_ADDR : assert always (s_fsm_state = IDLE) -> next (s_fsm_state = ADDR) abort not(s_reset_n); - -- psl ADDR_DATA : assert always (s_fsm_state = ADDR) -> next (s_fsm_state = DATA) abort not(s_reset_n); - -- psl DATA_IDLE : assert always (s_fsm_state = DATA) -> next (s_fsm_state = IDLE) abort not(s_reset_n); + -- psl IDLE_ADDR : assert always (s_fsm_state = IDLE and s_reset_n = '1') -> next (s_fsm_state = ADDR) abort not(s_reset_n) + -- report "FSM error: IDLE should be followed by ADDR state"; + + -- psl ADDR_DATA : assert always (s_fsm_state = ADDR and s_reset_n = '1') -> next (s_fsm_state = DATA) abort not(s_reset_n); + -- report "FSM error: ADDR should be followed by DATA state"; + + -- psl DATA_IDLE : assert always (s_fsm_state = DATA and s_reset_n = '1') -> next (s_fsm_state = IDLE) abort not(s_reset_n); + -- report "FSM error: DATA should be followed by IDLE state"; end architecture sim;