//---------------------------------------------------------------------------
//
//       ASSERT_IMPLICATION
//
//---------------------------------------------------------------------------
// NAME
//          ASSERT_IMPLICATION - An invariant concurrent assertion to ensure 
//              that a logical implication always evaluates TRUE.
//
//---------------------------------------------------------------------------

module assert_implication (clk, reset_n, antecendent_expr, consequent_expr);
// synopsys template
  input clk, reset_n, antecendent_expr, consequent_expr;
  parameter severity_level = 0;
  parameter options = 0;
  parameter msg="VIOLATION";

//synopsys translate_off
`ifdef ASSERT_ON

  parameter assert_name = "ASSERT_IMPLICATION";

  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 != 0) begin  // active low reset
    `endif
        if (antecendent_expr  == 1'b1 && consequent_expr  == 1'b0) begin
          ovl_error("");
        end
      end
  end
`endif
//synopsys translate_on

endmodule