// Accellera Standard V2.8.1 Open Verification Library (OVL).
// Accellera Copyright (c) 2005-2014. All rights reserved.

vunit assert_implication_assert_vunit (assert_implication_assert)
{
  default clock = (posedge clk);

  property ASSERT_IMPLICATION_P = always (
           reset_n && antecedent_expr -> consequent_expr);

  //Properties for X/Z checking

  property ASSERT_IMPLICATION_XZ_ON_ANT_EXP_P =
           always( xzcheck_enable && (!consequent_expr) -> !isunknown(antecedent_expr) abort(!reset_n) );

  property ASSERT_IMPLICATION_XZ_ON_CON_EXP_P =
           always( xzcheck_enable && antecedent_expr -> !isunknown(consequent_expr) 
                   abort(!reset_n) );

  A_ASSERT_IMPLICATION_P:
  assert ASSERT_IMPLICATION_P
  report "VIOLATION: ASSERT_IMPLICATION Checker Fires : Antecedent does not have consequent";

  A_ASSERT_IMPLICATION_XZ_ON_ANT_EXP_P:
  assert ASSERT_IMPLICATION_XZ_ON_ANT_EXP_P
  report "VIOLATION: ASSERT_IMPLICATION Checker Fires: antecedent_expr contains X or Z";

  A_ASSERT_IMPLICATION_XZ_ON_CON_EXP_P:
  assert ASSERT_IMPLICATION_XZ_ON_CON_EXP_P
  report "VIOLATION: ASSERT_IMPLICATION Checker Fires: consequent_expr contains X or Z";
}

vunit assert_implication_assume_vunit (assert_implication_assume)
{
  default clock = (posedge clk);
  
  property ASSERT_IMPLICATION_P = always (
           reset_n && antecedent_expr -> consequent_expr);
  
  //Properties for X/Z checking

  property ASSERT_IMPLICATION_XZ_ON_ANT_EXP_P =
           always( xzcheck_enable && (!consequent_expr) -> !isunknown(antecedent_expr) abort(!reset_n) );

  property ASSERT_IMPLICATION_XZ_ON_CON_EXP_P =
           always( xzcheck_enable && antecedent_expr -> !isunknown(consequent_expr) 
                   abort(!reset_n) );

  M_ASSERT_IMPLICATION_P:
  assume ASSERT_IMPLICATION_P;

  M_ASSERT_IMPLICATION_XZ_ON_ANT_EXP_P:
  assume ASSERT_IMPLICATION_XZ_ON_ANT_EXP_P;

  M_ASSERT_IMPLICATION_XZ_ON_CON_EXP_P:
  assume ASSERT_IMPLICATION_XZ_ON_CON_EXP_P;
}

vunit assert_implication_cover_vunit (assert_implication_cover)
{
  default clock = (posedge clk);
           
  cover_antecedent:
  cover {OVL_COVER_BASIC_ON && reset_n && antecedent_expr}
  report "COVERAGE REPORT: ASSERT_IMPLICATION Checker: antecedent covered";
}