//---------------------------------------------------------------------------
//
//       ASSERT_NO_TRANSITION
//
//---------------------------------------------------------------------------
// NAME
//          ASSERT_NO_TRANSITION - Check for specific illegal state 
//                 transitions.
//
//---------------------------------------------------------------------------
module assert_no_transition (clk, reset_n, test_expr, start_state, next_state);
// synopsys template
  parameter severity_level = 0;
  parameter width=1;
`ifdef ASSERT_V1_0_1 	// Previous version of the library
`else			// New version to allow for future options
  parameter options = 0;
`endif
  parameter msg="VIOLATION";
  input clk, reset_n;
  input [width-1:0] test_expr, start_state, next_state;

//synopsys translate_off
`ifdef ASSERT_ON

  reg [width-1:0] r_next_state, r_start_state;

  reg assert_state;
  initial assert_state = 1'b0;

  parameter assert_name = "ASSERT_NO_TRANSITION";

  integer error_count;
  initial error_count = 0;

  `include "ovl_task.h"

  `ifdef ASSERT_INIT_MSG
    initial
      ovl_init_msg; // Call the User Defined Init Message Routine
  `endif

  always @(posedge clk) begin
    `ifdef ASSERT_GLOBAL_RESET
      if (`ASSERT_GLOBAL_RESET != 1'b0) begin
    `else      
      if (reset_n != 1'b0) begin
    `endif
        if (assert_state == 1'b0) begin // INIT_STATE
          if (test_expr == start_state) begin
            assert_state  <= 1'b1; // CHECK_STATE
            r_start_state <= start_state;
            r_next_state  <= next_state;
          end
        end
        else begin                      // CHECK_STATE
          if (test_expr == r_next_state) begin
            ovl_error("");    // test_expr moves to unexpected state
            assert_state <= 1'b0;
          end
          else if (test_expr != r_start_state) begin
            assert_state <= 1'b0; // done ok.
          end
        end
      end
      else begin
        assert_state <= 1'b0;
      end
  end // always
`endif
//synopsys translate_on

endmodule