assert_fifo_index_logic.sv

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
          if ((cnt + push) <= depth) begin
            cnt <= cnt + push;
          end
        end
        else if ({push!=0,pop!=0} == 2'b01) begin // pop
          if (cnt >= pop) begin
            cnt <= cnt - pop;
          end
        end
        else if ({push!=0,pop!=0} == 2'b11) begin // push & pop
          if (!simultaneous_push_pop) begin
            //ILLEGAL PUSH AND POP
          end
          else begin
            if ((cnt + push - pop) > depth) begin
              //OVERFLOW"
            end
            else if ((cnt + push) < pop) begin
              //UNDERFLOW
            end
            else begin
              cnt <= cnt + push - pop;
            end
          end
        end
      end
      else begin
        cnt <= 0;
      end
  end

`endif // OVL_SHARED_CODE

  property ASSERT_FIFO_INDEX_OVERFLOW_P;
  @(posedge clk)
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  push && !(!simultaneous_push_pop && push && pop) |-> ((cnt + push - pop) <= depth);
  endproperty

  property ASSERT_FIFO_INDEX_UNDEFLOW_P;
  @(posedge clk)
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  pop && !(!simultaneous_push_pop && push && pop) |-> ((cnt + push) >= pop);
  endproperty

  property ASSERT_FIFO_INDEX_ILLEGAL_PUSH_POP_P;
  @(posedge clk)
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  !(push && pop);
  endproperty

`ifdef OVL_ASSERT_ON

  generate

    case (property_type)
      `OVL_ASSERT : begin

        A_ASSERT_FIFO_INDEX_OVERFLOW_P:
        assert property (ASSERT_FIFO_INDEX_OVERFLOW_P)
        else ovl_error_t("OVERFLOW");

        A_ASSERT_FIFO_INDEX_UNDEFLOW_P:
        assert property (ASSERT_FIFO_INDEX_UNDEFLOW_P)
        else ovl_error_t("UNDERFLOW");

        if (!simultaneous_push_pop) begin
          A_ASSERT_FIFO_INDEX_ILLEGAL_PUSH_POP_P:
          assert property (ASSERT_FIFO_INDEX_ILLEGAL_PUSH_POP_P)
          else ovl_error_t("ILLEGAL PUSH AND POP");
        end
      end
      `OVL_ASSUME : begin

        M_ASSERT_FIFO_INDEX_OVERFLOW_P:
        assume property (ASSERT_FIFO_INDEX_OVERFLOW_P);

        M_ASSERT_FIFO_INDEX_UNDEFLOW_P:
        assume property (ASSERT_FIFO_INDEX_UNDEFLOW_P);

        if (!simultaneous_push_pop) begin
          M_ASSERT_FIFO_INDEX_ILLEGAL_PUSH_POP_P:
          assume property (ASSERT_FIFO_INDEX_ILLEGAL_PUSH_POP_P);
        end
      end
      default     : ovl_error_t("");
    endcase

  endgenerate

`endif // OVL_ASSERT_ON

`ifdef OVL_COVER_ON

generate

 if (coverage_level != `OVL_COVER_NONE) begin

  cover_fifo_full:
  cover property ( @(posedge clk) ((cnt != depth) && (`OVL_RESET_SIGNAL != 1'b0)
                                  ##1
                                   (cnt == depth) && (`OVL_RESET_SIGNAL != 1'b0)
                                  )
                 )
                 ovl_cover_t("fifo_full covered");

  cover_fifo_empty:
  cover property ( @(posedge clk) ((cnt != 0) && (`OVL_RESET_SIGNAL != 1'b0)
                                  ##1
                                   (cnt == 0) && (`OVL_RESET_SIGNAL != 1'b0)
                                  )
                 )
                 ovl_cover_t("fifo_full covered");

  cover_fifo_push:
  cover property ( @(posedge clk) ((`OVL_RESET_SIGNAL != 1'b0) && push))
                 ovl_cover_t("fifo_push covered");

  cover_fifo_pop:
  cover property ( @(posedge clk) ((`OVL_RESET_SIGNAL != 1'b0) && pop))
                 ovl_cover_t("fifo_pop covered");

  cover_fifo_simultaneous_push_pop:
  cover property ( @(posedge clk) ((`OVL_RESET_SIGNAL != 1'b0) && push && pop))
                 ovl_cover_t("fifo_simultaneous_push_pop covered");

 end

endgenerate

`endif // OVL_COVER_ON