assert_fifo_index_logic.v

OVL——基于断言的verilog验证 Verilog数字系统设计:RTL综合、测试平台与验证

// Accellera Standard V1.0 Open Verification Library (OVL).
// Accellera Copyright (c) 2005. All rights reserved.

  parameter assert_name = "ASSERT_FIFO_INDEX";

  integer cnt;
  initial begin
    cnt=0;
    if (depth==0) ovl_error_t("Depth parameter value must be > 0");
  end

  `include "std_ovl_task.h"
  
  `ifdef OVL_INIT_MSG
    initial
      ovl_init_msg_t; // Call the User Defined Init Message Routine
  `endif

`ifdef OVL_SHARED_CODE

  always @(posedge clk) begin
    `ifdef OVL_GLOBAL_RESET
      if (`OVL_GLOBAL_RESET != 1'b0) begin
    `else
      if (reset_n != 0) begin // active low reset
    `endif
        if ({push!=0,pop!=0} == 2'b10) begin // push
          `ifdef OVL_COVER_ON
            if (coverage_level != `OVL_COVER_NONE)
              ovl_cover_t("fifo_push covered");
          `endif // OVL_COVER_ON
          if ((cnt + push) > depth) begin
             ovl_error_t("OVERFLOW");
          end
          else begin
            cnt <= cnt + push;
            `ifdef OVL_COVER_ON
              if (coverage_level != `OVL_COVER_NONE)
                if ((cnt + push) == depth)
                  ovl_cover_t("fifo_full covered");
            `endif // OVL_COVER_ON
          end
        end
        else if ({push!=0,pop!=0} == 2'b01) begin // pop
          `ifdef OVL_COVER_ON
            if (coverage_level != `OVL_COVER_NONE)
              ovl_cover_t("fifo_pop covered");
          `endif // OVL_COVER_ON
          if (cnt < pop) begin
             ovl_error_t("UNDERFLOW");
          end
          else begin
            cnt <= cnt - pop;
            `ifdef OVL_COVER_ON
              if (coverage_level != `OVL_COVER_NONE)
                if ((cnt - pop) == 0)
                  ovl_cover_t("fifo_empty covered");
            `endif // OVL_COVER_ON
          end
        end
        else if ({push!=0,pop!=0} == 2'b11) begin // push & pop
          `ifdef OVL_COVER_ON
            if (coverage_level != `OVL_COVER_NONE) begin
              ovl_cover_t("fifo_simultaneous_push_pop covered");
            end
          `endif // OVL_COVER_ON
          if (!simultaneous_push_pop) begin
             ovl_error_t("ILLEGAL PUSH AND POP");
          end
          else begin
            if ((cnt + push - pop) > depth) begin
              ovl_error_t("OVERFLOW");
            end
            if ((cnt + push) < pop) begin
              ovl_error_t("UNDERFLOW");
            end
            else begin
              cnt <= cnt + push - pop;
              `ifdef OVL_COVER_ON
                if (coverage_level != `OVL_COVER_NONE) begin
                  if ((cnt + push - pop) == depth)
                    ovl_cover_t("fifo_full covered");
                  else if ((cnt + push - pop) == 0)
                    ovl_cover_t("fifo_empty covered");
                end
              `endif // OVL_COVER_ON
            end
          end
        end
      end
      else begin
        cnt <= 0;
      end
  end

`endif // OVL_SHARED_CODE