//---------------------------------------------------------------------------
//
//       ASSERT_NEVER_GO_X_OR_Z
//
//---------------------------------------------------------------------------
// NAME
//          ASSERT_NEVER_GO_X_OR_Z - An invariant concurrent assertion to 
//                                   ensure that no bits of a variable can
//                                   transition from a known 0 or 1 to an
//                                   unknown X or Z (at all times)
//
//---------------------------------------------------------------------------
module assert_never_go_x_or_z (reset_n, test_expr);
// synopsys template
  parameter severity_level = 0;
  parameter width=1;
  parameter msg="VIOLATION";
  input reset_n;
  input [width-1:0] test_expr;

`ifdef ASSERT_ON
  `ifdef ASSERT_OVL_VERILOG
  `else
    `define ASSERT_OVL_VERILOG
  `endif
`endif

//synopsys translate_off
`ifdef ASSERT_OVL_VERILOG

  parameter assert_name = "ASSERT_NEVER_GO_X_OR_Z";

  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 @(test_expr) begin // Incomplete Sensitivity-List (see Notes below)
    `ifdef ASSERT_GLOBAL_RESET
      if (`ASSERT_GLOBAL_RESET != 1'b0) begin
    `else      
      if (reset_n != 1'b0) begin
    `endif
        if ((|(test_expr ^ test_expr)) == 1'b0) // can only be 1'b0 or 1'bx
           begin
              // NOP - signal contains no X or Z
           end
        else
           ovl_error("");
      end // if (<reset>)
   end // always

`endif
//synopsys translate_on

endmodule

// Notes
// =====
// 1) Deliberately did not add "or reset_n" to the sensitivity list. If this
//    is done then any DFFs that are not reset will cause an error on the 
//    edge that the reset de-asserts (as there's still an X in the DFF and
//    the process would be activated by the edge on reset).
//
// 2) Rather than disabling this during reset, you could avoid the reset signal
//    altogether. However, you would need to put a #1 before the test_expr
//    if-statement (to avoid the initial transition to X at time 0).