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

vunit assert_window_assert_vunit (assert_window_assert)
{
  default clock = (posedge clk);
  
  property ASSERT_WINDOW_P = always (
           ({rose(start_event) && !end_event;(!(end_event && test_expr))[*1:inf]} |-> {test_expr}) 
           abort(!reset_n));
 
 //Properties for X/Z checking

  property ASSERT_WINDOW_XZ_ON_START_EVENT_P =
           always( xzcheck_enable && (!(xzcheck_window)) -> !isunknown(start_event)
                  abort(!reset_n) );

  property ASSERT_WINDOW_XZ_ON_TEST_EXPR_P =
           always( xzcheck_enable && xzcheck_window -> !isunknown(test_expr)
                  abort(!reset_n) );

  property ASSERT_WINDOW_XZ_ON_END_EVENT_P =
           always( xzcheck_enable && xzcheck_window -> !isunknown(end_event)
                  abort(!reset_n) );

  A_ASSERT_WINDOW_P:
  assert ASSERT_WINDOW_P
  report "VIOLATION: ASSERT_WINDOW Checker Fires : Test expression changed value during an open event window";

  A_ASSERT_WINDOW_XZ_ON_START_EVENT_P:
  assert ASSERT_WINDOW_XZ_ON_START_EVENT_P
  report "VIOLATION: ASSERT_WINDOW Checker Fires: start_event contains X or Z";

  A_ASSERT_WINDOW_XZ_ON_TEST_EXPR_P:
  assert ASSERT_WINDOW_XZ_ON_TEST_EXPR_P
  report "VIOLATION: ASSERT_WINDOW Checker Fires: test_expr contains X or Z";

  A_ASSERT_WINDOW_XZ_ON_END_EVENT_P:
  assert ASSERT_WINDOW_XZ_ON_END_EVENT_P
  report "VIOLATION: ASSERT_WINDOW Checker Fires: end_event contains X or Z";
}

vunit assert_window_assume_vunit (assert_window_assume)
{
  default clock = (posedge clk);
  
  property ASSERT_WINDOW_P = always (
           ({rose(start_event) && !end_event;(!(end_event && test_expr))[*1:inf]} |-> {test_expr})
           abort(!reset_n));

 //Properties for X/Z checking

  property ASSERT_WINDOW_XZ_ON_START_EVENT_P =
           always( xzcheck_enable && (!(xzcheck_window)) -> !isunknown(start_event)
                  abort(!reset_n) );

  property ASSERT_WINDOW_XZ_ON_TEST_EXPR_P =
           always( xzcheck_enable && xzcheck_window -> !isunknown(test_expr)
                  abort(!reset_n) );

  property ASSERT_WINDOW_XZ_ON_END_EVENT_P =
           always( xzcheck_enable && xzcheck_window -> !isunknown(end_event)
                  abort(!reset_n) );

  M_ASSERT_WINDOW_P:
  assume ASSERT_WINDOW_P;

  M_ASSERT_WINDOW_XZ_ON_START_EVENT_P:
  assume ASSERT_WINDOW_XZ_ON_START_EVENT_P;

  M_ASSERT_WINDOW_XZ_ON_TEST_EXPR_P:
  assume ASSERT_WINDOW_XZ_ON_TEST_EXPR_P;

  M_ASSERT_WINDOW_XZ_ON_END_EVENT_P:
  assume ASSERT_WINDOW_XZ_ON_END_EVENT_P;
}

vunit assert_window_cover_vunit (assert_window_cover)
{
  default clock = (posedge clk);
                                                                                                                                                 
  cover_window_open:
  cover {OVL_COVER_BASIC_ON && reset_n && rose(start_event) & !end_event}
  report "COVERAGE REPORT : ASSERT_WIN_CHANGE Checker: window_open covered";
                                                                                      
  cover_window:
  cover {OVL_COVER_BASIC_ON && reset_n && rose(start_event) & !end_event; (reset_n && !end_event)[*]; reset_n && end_event}
  report "COVERAGE REPORT : ASSERT_WIN_CHANGE Checker: window covered";

}